equal
deleted
inserted
replaced
11 structure O = ThyOutput; |
11 structure O = ThyOutput; |
12 |
12 |
13 |
13 |
14 (* misc utils *) |
14 (* misc utils *) |
15 |
15 |
16 val clean_string = |
16 val clean_string = translate_string |
17 translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c); |
17 (fn "_" => "-" |
|
18 | ">" => "$>$" |
|
19 | "#" => "\\#" |
|
20 | "{" => "\\{" |
|
21 | "}" => "\\}" |
|
22 | c => c); |
18 |
23 |
19 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
24 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
20 |
25 |
21 fun tweak_line s = |
26 fun tweak_line s = |
22 if ! O.display then s else Symbol.strip_blanks s; |
27 if ! O.display then s else Symbol.strip_blanks s; |