equal
deleted
inserted
replaced
28 | clean_name "_" = "underscore" |
28 | clean_name "_" = "underscore" |
29 | clean_name "{" = "braceleft" |
29 | clean_name "{" = "braceleft" |
30 | clean_name "}" = "braceright" |
30 | clean_name "}" = "braceright" |
31 | clean_name s = s |> translate_string (fn "_" => "-" | c => c); |
31 | clean_name s = s |> translate_string (fn "_" => "-" | c => c); |
32 |
32 |
33 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
33 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
34 |
34 |
35 fun tweak_line s = |
35 fun tweak_line s = |
36 if ! O.display then s else Symbol.strip_blanks s; |
36 if ! O.display then s else Symbol.strip_blanks s; |
37 |
37 |
38 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
38 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |