From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 26 Sep 2005 16:30:36 +0000 (+0000)
Subject: strip heading '\' on Mo s
X-Git-Tag: V_0_7_2_3~306
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88ac88bc07c117b45d17415d7df635bf7b5f7ccd;p=helm.git

strip heading '\' on Mo s
---

diff --git a/helm/ocaml/cic_notation/mpresentation.ml b/helm/ocaml/cic_notation/mpresentation.ml
index db05f31be..1303d1eb7 100644
--- a/helm/ocaml/cic_notation/mpresentation.ml
+++ b/helm/ocaml/cic_notation/mpresentation.ml
@@ -108,7 +108,14 @@ let print_mpres obj_printer mpres =
     function
       Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
     | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
-    | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
+    | Mo (attr,s) ->
+        let s =
+          let len = String.length s in
+          if len > 1 && s.[0] = '\\'
+          then String.sub s 1 (len - 1)
+          else s
+        in
+        X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
     | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
     | Mspace attr -> X.xml_empty ~prefix "mspace" attr
     | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)