]> matita.cs.unibo.it Git - helm.git/commitdiff
add \\ in front of tex macros
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 23 Jun 2008 15:06:12 +0000 (15:06 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 23 Jun 2008 15:06:12 +0000 (15:06 +0000)
helm/software/components/syntax_extensions/utf8Macro.ml

index 00e10f18335747f9dd50ff23a43632c923ae29d8..c95282d58a061d1569a199a59a5ce582e46350d4 100644 (file)
@@ -45,7 +45,10 @@ let tex_of_unicode s =
  if s = " " then [""]
  else
   try
-    let alt = Hashtbl.find_all Utf8MacroTable.utf82macro s in
+    let alt = 
+      List.map (fun x -> "\\"^x) 
+       (Hashtbl.find_all Utf8MacroTable.utf82macro s)
+    in
     List.sort 
       (fun x y -> Pervasives.compare (String.length x) (String.length y)) 
       alt