From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 28 Jul 2005 13:21:23 +0000 (+0000)
Subject: added pretty printing of unicode symbols to TeX like macro
X-Git-Tag: V_0_7_2~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f62c6339bd0578870c14a56c5d93c6280a31c04;p=helm.git

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