From 1f62c6339bd0578870c14a56c5d93c6280a31c04 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 28 Jul 2005 13:21:23 +0000
Subject: [PATCH] added pretty printing of unicode symbols to TeX like macro

---
 helm/ocaml/cic_notation/boxPp.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

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
-- 
2.39.2