pango escape fixed

[helm.git] / helm / software / matita / matitaGtkMisc.ml

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index 9c00dfddef4aa1b7879026c85e12fa1df0c3700d..872780540197ab9f2f98eaf2c42718606af391cb 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -411,4 +411,13 @@ let utf8_string_length s =
   if BuildTimeConf.debug then
     assert(Glib.Utf8.validate s);
   Glib.Utf8.length s
+
+let escape_pango_markup text =
+   let text = Pcre.replace ~pat:"&" ~templ:"&" text in
+   let text = Pcre.replace ~pat:"<" ~templ:"&lt;" text in
+   let text = Pcre.replace ~pat:"'" ~templ:"&apos;" text in
+   let text = Pcre.replace ~pat:"\"" ~templ:"&quot;" text in
+   text
+;;
+