From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 23 Jun 2008 15:06:12 +0000 (+0000)
Subject: add \\ in front of tex macros
X-Git-Tag: make_still_working~4999
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d4c63a0ff7d44e4e361fc4aeca8028a77d39568;p=helm.git

add \\ in front of tex macros
---

diff --git a/helm/software/components/syntax_extensions/utf8Macro.ml b/helm/software/components/syntax_extensions/utf8Macro.ml
index 00e10f183..c95282d58 100644
--- a/helm/software/components/syntax_extensions/utf8Macro.ml
+++ b/helm/software/components/syntax_extensions/utf8Macro.ml
@@ -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