]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/syntax_extensions/utf8Macro.ml
Previous commit reverted, as explained in that log.
[helm.git] / 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