X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FboxPp.ml;h=b9bb9fbbd5badc06ef55a36ca418471731559db2;hb=db9b735ff1192a7e308eaa0c073fa360f76f0ce2;hp=53149877ea73a1eb71e3c5b2f75ec4f7f78df552;hpb=8f34d1d64451220aba4de24cf322bdd826ff7248;p=helm.git

diff --git a/components/content_pres/boxPp.ml b/components/content_pres/boxPp.ml
index 53149877e..b9bb9fbbd 100644
--- a/components/content_pres/boxPp.ml
+++ b/components/content_pres/boxPp.ml
@@ -193,13 +193,14 @@ let render_to_strings choose_action size markup =
     | Pres.Mgliph (_, s) -> fixed_rendering s
     | Pres.Mo (_, s) ->
         let s =
-          if String.length s > 1 then
-            (* heuristic to guess which operators need to be expanded in their
-             * TeX like format *)
-            Utf8Macro.tex_of_unicode s ^ " "
-          else s
+         if String.length s = 1 && Char.code s.[0] < 128 then
+          s
+         else
+          match Utf8Macro.tex_of_unicode s with
+             Some s -> s ^ " "
+           | None -> s
         in
-        fixed_rendering s
+         fixed_rendering s
     | Pres.Mspace _ -> fixed_rendering string_space
     | Pres.Mrow (attrs, children) ->
         let children' = List.map aux_mpres children in