From 9e1d0c4f6ddf36cd691ef0d3c95aaa7f694977f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Aug 2008 22:47:43 +0000 Subject: [PATCH] ... --- helm/software/matita/matitaGui.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 96cd079e9..9e8cfd86c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1379,7 +1379,12 @@ class interpModel = let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris -= += + + let text = Pcre.replace ~pat:"<" ~templ:"<" text in + let text = Pcre.replace ~pat:"'" ~templ:"'" text in + let text = Pcre.replace ~pat:"\"" ~templ:""" text in + let text = Pcre.replace ~pat:">" ~templ:">" text in let gui = instance () in let dialog = gui#newUriDialog () in dialog#uriEntryHBox#misc#hide (); -- 2.39.2