doc-src/antiquote_setup.ML
changeset 26910 aa6357b39212
parent 26903 0542898ab667
child 27353 71c4dd53d4cb
--- a/doc-src/antiquote_setup.ML	Thu May 15 20:02:39 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Thu May 15 20:02:40 2008 +0200
@@ -25,6 +25,7 @@
 fun clean_name "\\<dots>" = "dots"
   | clean_name ".." = "ddot"
   | clean_name "." = "dot"
+  | clean_name "_" = "underscore"
   | clean_name "{" = "braceleft"
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate_string (fn "_" => "-" | c => c);