changeset 27809 | a1e409db516b |
parent 27353 | 71c4dd53d4cb |
child 28217 | 21f0c2de0a38 |
--- a/doc-src/antiquote_setup.ML Sat Aug 09 12:28:13 2008 +0200 +++ b/doc-src/antiquote_setup.ML Sat Aug 09 22:43:46 2008 +0200 @@ -30,7 +30,7 @@ | clean_name "}" = "braceright" | clean_name s = s |> translate_string (fn "_" => "-" | c => c); -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; +val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; fun tweak_line s = if ! O.display then s else Symbol.strip_blanks s;