--- a/doc-src/antiquote_setup.ML Fri Feb 13 19:41:14 2009 +0100
+++ b/doc-src/antiquote_setup.ML Sat Feb 14 21:34:12 2009 +0100
@@ -12,13 +12,16 @@
(* misc utils *)
-val clean_string = translate_string
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
(fn "_" => "\\_"
| "<" => "$<$"
| ">" => "$>$"
| "#" => "\\#"
| "{" => "\\{"
| "}" => "\\}"
+ | "\\<dash>" => "-"
| c => c);
fun clean_name "\\<dots>" = "dots"
@@ -27,7 +30,7 @@
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
(* verbatim text *)