added pretty printing of unicode symbols to TeX like macro

diff --git a/helm/ocaml/cic_notation/boxPp.ml b/helm/ocaml/cic_notation/boxPp.ml
index a843625fc70d689dd3e26e65fe111198eefb2bcd..ddb9d3b82af51960b832880e0ee90406181a92d2 100644 (file)
--- 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