67 fun get_index {main = m, minor = n} = |
67 fun get_index {main = m, minor = n} = |
68 (if n = NoString |
68 (if n = NoString |
69 then implode ["\\index{", get_indstring m, "}"] |
69 then implode ["\\index{", get_indstring m, "}"] |
70 else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"]) |
70 else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"]) |
71 |
71 |
|
72 fun get_str_index {main = m, minor = n} = |
|
73 (case n of |
|
74 Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] |
|
75 | _ => "") |
|
76 |
72 fun output_indexed ind txt = |
77 fun output_indexed ind txt = |
73 txt |> output |
78 txt |> output |
74 |> prefix (get_index ind) |
79 |> prefix (get_index ind) |
|
80 |> prefix (get_str_index ind) |
75 |
81 |
76 fun boolean "" = true |
82 fun boolean "" = true |
77 | boolean "true" = true |
83 | boolean "true" = true |
78 | boolean "false" = false |
84 | boolean "false" = false |
79 | boolean s = error ("Bad boolean value: " ^ quote s); |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |