X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FboxPp.ml;h=ddb9d3b82af51960b832880e0ee90406181a92d2;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a843625fc70d689dd3e26e65fe111198eefb2bcd;hpb=2fdc0e2718552c0d300b38a6f677873f02ee2217;p=helm.git

diff --git a/helm/ocaml/cic_notation/boxPp.ml b/helm/ocaml/cic_notation/boxPp.ml
index a843625fc..ddb9d3b82 100644
--- a/helm/ocaml/cic_notation/boxPp.ml
+++ b/helm/ocaml/cic_notation/boxPp.ml
@@ -186,10 +186,18 @@ let render_to_strings size markup =
     function
     | Pres.Mi (_, s)
     | Pres.Mn (_, s)
-    | Pres.Mo (_, s)
     | Pres.Mtext (_, s)
     | Pres.Ms (_, s)
     | 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
+        in
+        fixed_rendering s
     | Pres.Mspace _ -> fixed_rendering string_space
     | Pres.Mrow (attrs, children) ->
         let children' = List.map aux_mpres children in