clean_string: handle { };
authorwenzelm
Fri, 02 May 2008 16:36:29 +0200
changeset 26768844068d16ba0
parent 26767 cc127cc0951b
child 26769 5b8382d495be
clean_string: handle { };
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Fri May 02 16:36:05 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Fri May 02 16:36:29 2008 +0200
     1.3 @@ -13,8 +13,13 @@
     1.4  
     1.5  (* misc utils *)
     1.6  
     1.7 -val clean_string =
     1.8 -  translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c);
     1.9 +val clean_string = translate_string
    1.10 +  (fn "_" => "-"
    1.11 +    | ">" => "$>$"
    1.12 +    | "#" => "\\#"
    1.13 +    | "{" => "\\{"
    1.14 +    | "}" => "\\}"
    1.15 +    | c => c);
    1.16  
    1.17  val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
    1.18