doc-src/antiquote_setup.ML
changeset 29736 ec3fc818b82e
parent 29726 5f91ff5c03a2
child 30120 aaa4667285c8
equal deleted inserted replaced
29735:1da96affdefe 29736:ec3fc818b82e
    10 structure O = ThyOutput;
    10 structure O = ThyOutput;
    11 
    11 
    12 
    12 
    13 (* misc utils *)
    13 (* misc utils *)
    14 
    14 
    15 val clean_string = translate_string
    15 fun translate f = Symbol.explode #> map f #> implode;
       
    16 
       
    17 val clean_string = translate
    16   (fn "_" => "\\_"
    18   (fn "_" => "\\_"
    17     | "<" => "$<$"
    19     | "<" => "$<$"
    18     | ">" => "$>$"
    20     | ">" => "$>$"
    19     | "#" => "\\#"
    21     | "#" => "\\#"
    20     | "{" => "\\{"
    22     | "{" => "\\{"
    21     | "}" => "\\}"
    23     | "}" => "\\}"
       
    24     | "\\<dash>" => "-"
    22     | c => c);
    25     | c => c);
    23 
    26 
    24 fun clean_name "\\<dots>" = "dots"
    27 fun clean_name "\\<dots>" = "dots"
    25   | clean_name ".." = "ddot"
    28   | clean_name ".." = "ddot"
    26   | clean_name "." = "dot"
    29   | clean_name "." = "dot"
    27   | clean_name "_" = "underscore"
    30   | clean_name "_" = "underscore"
    28   | clean_name "{" = "braceleft"
    31   | clean_name "{" = "braceleft"
    29   | clean_name "}" = "braceright"
    32   | clean_name "}" = "braceright"
    30   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
    33   | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
    31 
    34 
    32 
    35 
    33 (* verbatim text *)
    36 (* verbatim text *)
    34 
    37 
    35 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    38 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";