added default for matita.noiinertypes

[helm.git] / components / syntax_extensions / utf8Macro.ml

diff --git a/components/syntax_extensions/utf8Macro.ml b/components/syntax_extensions/utf8Macro.ml
index e5fca10c48cc06e3a428865ea94190758f7cbc3f..36d6b175d713cd213ae540bdb9aa953e8f80efaf 100644 (file)
--- a/components/syntax_extensions/utf8Macro.ml
+++ b/components/syntax_extensions/utf8Macro.ml
@@ -41,7 +41,10 @@ let unicode_of_tex s =
   with Macro_not_found _ -> s
 
 let tex_of_unicode s =
+ (*WARNING: the space below is a nbsp (0x00A0), not a normal space *)
+ if s = " " then Some ""
+ else
   try
-    "\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s
-  with Not_found -> s
+    Some ("\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s)
+  with Not_found -> None