author | wenzelm |
Thu, 15 May 2008 20:02:40 +0200 | |
changeset 26910 | aa6357b39212 |
parent 26909 | f42d638c5f07 |
child 26911 | 871cc7f11034 |
1.1 --- a/doc-src/antiquote_setup.ML Thu May 15 20:02:39 2008 +0200 1.2 +++ b/doc-src/antiquote_setup.ML Thu May 15 20:02:40 2008 +0200 1.3 @@ -25,6 +25,7 @@ 1.4 fun clean_name "\\<dots>" = "dots" 1.5 | clean_name ".." = "ddot" 1.6 | clean_name "." = "dot" 1.7 + | clean_name "_" = "underscore" 1.8 | clean_name "{" = "braceleft" 1.9 | clean_name "}" = "braceright" 1.10 | clean_name s = s |> translate_string (fn "_" => "-" | c => c);