equal
deleted
inserted
replaced
10 structure O = ThyOutput; |
10 structure O = ThyOutput; |
11 |
11 |
12 |
12 |
13 (* misc utils *) |
13 (* misc utils *) |
14 |
14 |
15 val clean_string = translate_string |
15 fun translate f = Symbol.explode #> map f #> implode; |
|
16 |
|
17 val clean_string = translate |
16 (fn "_" => "\\_" |
18 (fn "_" => "\\_" |
17 | "<" => "$<$" |
19 | "<" => "$<$" |
18 | ">" => "$>$" |
20 | ">" => "$>$" |
19 | "#" => "\\#" |
21 | "#" => "\\#" |
20 | "{" => "\\{" |
22 | "{" => "\\{" |
21 | "}" => "\\}" |
23 | "}" => "\\}" |
|
24 | "\\<dash>" => "-" |
22 | c => c); |
25 | c => c); |
23 |
26 |
24 fun clean_name "\\<dots>" = "dots" |
27 fun clean_name "\\<dots>" = "dots" |
25 | clean_name ".." = "ddot" |
28 | clean_name ".." = "ddot" |
26 | clean_name "." = "dot" |
29 | clean_name "." = "dot" |
27 | clean_name "_" = "underscore" |
30 | clean_name "_" = "underscore" |
28 | clean_name "{" = "braceleft" |
31 | clean_name "{" = "braceleft" |
29 | clean_name "}" = "braceright" |
32 | clean_name "}" = "braceright" |
30 | clean_name s = s |> translate_string (fn "_" => "-" | c => c); |
33 | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c); |
31 |
34 |
32 |
35 |
33 (* verbatim text *) |
36 (* verbatim text *) |
34 |
37 |
35 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
38 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |