From 88ac88bc07c117b45d17415d7df635bf7b5f7ccd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 16:30:36 +0000 Subject: [PATCH] strip heading '\' on Mo s --- helm/ocaml/cic_notation/mpresentation.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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) -- 2.39.2