25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
26 #> space_implode "\\isasep\\isanewline%\n" |
26 #> space_implode "\\isasep\\isanewline%\n" |
27 #> enclose "\\isa{" "}") |
27 #> enclose "\\isa{" "}") |
28 end |
28 end |
29 |
29 |
30 datatype qstring = |
30 datatype indstring = |
31 NoString |
31 NoString |
32 | Plain of string |
32 | Plain of string |
33 | Code of string |
33 | Code of string |
34 | IStruct of string |
34 | Struct of string |
35 |
35 |
36 datatype entry = |
36 fun translate_string f = Symbol.explode #> map f #> implode; |
37 No_Entry |
|
38 | Default |
|
39 | Explicit of string |
|
40 |
37 |
41 val index = ref No_Entry |
38 val clean_string = translate_string |
42 |
|
43 fun translate f = Symbol.explode #> map f #> implode; |
|
44 |
|
45 val clean_string = translate |
|
46 (fn "_" => "\\_" |
39 (fn "_" => "\\_" |
47 | "#" => "\\#" |
40 | "#" => "\\#" |
48 | "<" => "\\isacharless" |
41 | "<" => "\\isacharless" |
49 | ">" => "\\isachargreater" |
42 | ">" => "\\isachargreater" |
50 | "{" => "\\{" |
43 | "{" => "\\{" |
51 | "|" => "\\isacharbar" |
44 | "|" => "\\isacharbar" |
52 | "}" => "\\}" |
45 | "}" => "\\}" |
53 | "$" => "\\isachardollar" |
46 | "$" => "\\isachardollar" |
54 | "!" => "\\isacharbang" |
47 | "!" => "\\isacharbang" |
55 | "\<dash>" => "-" |
48 | "\<dash>" => "-" |
56 | c => c); |
49 | c => c) |
57 |
50 |
58 fun get_word str = |
51 fun get_word str = |
59 let |
52 let |
60 fun only_letters [] = true |
53 fun only_letters [] = true |
61 | only_letters (x::xs) = |
54 | only_letters (x::xs) = |
62 if (Symbol.is_ascii_blank x) then false else only_letters xs |
55 if (Symbol.is_ascii_blank x) then false else only_letters xs |
63 in |
56 in |
64 if (only_letters (Symbol.explode str)) then (clean_string str) |
57 if only_letters (Symbol.explode str) |
65 else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str) |
58 then clean_string str |
|
59 else error ("Only single word allowed! Error with " ^ quote str) |
66 end |
60 end |
67 |
61 |
68 fun get_qstring NoString = "" |
62 fun get_indstring NoString = "" |
69 | get_qstring (Plain s) = get_word s |
63 | get_indstring (Plain s) = get_word s |
70 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
64 | get_indstring (Code s) = let val w = get_word s in implode[w, "@{\\tt\\slshape{}", w, "}"] end |
71 | get_qstring (IStruct s) = "in {\\tt\\slshape{}" ^ (get_word s) ^ "}" |
65 | get_indstring (Struct s) = implode ["in {\\tt\\slshape{}", get_word s, "}"] |
72 |
66 |
73 fun is_empty_qstr (Plain "") = true |
67 fun get_index {main = m, minor = n} = |
74 | is_empty_qstr (Code "") = true |
|
75 | is_empty_qstr _ = false |
|
76 |
|
77 fun get_index_info {main = m, minor = n} = |
|
78 (if n = NoString |
68 (if n = NoString |
79 then "\\index{" ^ (get_qstring m) ^ "}" |
69 then implode ["\\index{", get_indstring m, "}"] |
80 else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring n) ^ "}") |
70 else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"]) |
81 |
71 |
82 fun index_entry entry index_info = |
72 fun output_indexed ind txt = |
83 case entry of |
|
84 No_Entry => I |
|
85 | Explicit s => prefix s |
|
86 | Default => prefix (get_index_info index_info) |
|
87 |
|
88 fun output_indexed txt index_info = |
|
89 txt |> output |
73 txt |> output |
90 |> index_entry (!index) index_info |
74 |> prefix (get_index ind) |
91 |
75 |
92 fun boolean "" = true |
76 fun boolean "" = true |
93 | boolean "true" = true |
77 | boolean "true" = true |
94 | boolean "false" = false |
78 | boolean "false" = false |
95 | boolean s = error ("Bad boolean value: " ^ quote s); |
79 | boolean s = error ("Bad boolean value: " ^ quote s); |
96 |
80 |
97 fun explicit "" = Default |
|
98 | explicit s = Explicit s |
|
99 |
|
100 |
|
101 val _ = ThyOutput.add_options |
81 val _ = ThyOutput.add_options |
102 [("gray", Library.setmp gray o boolean), |
82 [("gray", Library.setmp gray o boolean), |
103 ("linenos", Library.setmp linenos o boolean), |
83 ("linenos", Library.setmp linenos o boolean)] |
104 ("index", Library.setmp index o explicit)] |
|
105 |
|
106 |
84 |
107 end |
85 end |