1.1 --- a/doc-src/antiquote_setup.ML	Fri Feb 13 19:41:14 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Feb 14 21:34:12 2009 +0100
     1.3 @@ -12,13 +12,16 @@
     1.4  
     1.5  (* misc utils *)
     1.6  
     1.7 -val clean_string = translate_string
     1.8 +fun translate f = Symbol.explode #> map f #> implode;
     1.9 +
    1.10 +val clean_string = translate
    1.11    (fn "_" => "\\_"
    1.12      | "<" => "$<$"
    1.13      | ">" => "$>$"
    1.14      | "#" => "\\#"
    1.15      | "{" => "\\{"
    1.16      | "}" => "\\}"
    1.17 +    | "\\<dash>" => "-"
    1.18      | c => c);
    1.19  
    1.20  fun clean_name "\\<dots>" = "dots"
    1.21 @@ -27,7 +30,7 @@
    1.22    | clean_name "_" = "underscore"
    1.23    | clean_name "{" = "braceleft"
    1.24    | clean_name "}" = "braceright"
    1.25 -  | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
    1.26 +  | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
    1.27  
    1.28  
    1.29  (* verbatim text *)