nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index 09a5c3982b3cd4e27b21f71f9a7532ebe3d3d987..872780540197ab9f2f98eaf2c42718606af391cb 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -411,33 +411,13 @@ let utf8_string_length s =
   if BuildTimeConf.debug then
     assert(Glib.Utf8.validate s);
   Glib.Utf8.length s
-    
-let new_search_win title text =
-     let w = new MatitaGeneratedGui.searchWin () in
-     let t = 
-       GSourceView.source_view ~auto_indent:false ~editable:false ()
-     in
-     let callback () = 
-       let text = w#entrySearch#text in
-       let highlight start end_ =
-         t#source_buffer#move_mark `INSERT ~where:start;
-         t#source_buffer#move_mark `SEL_BOUND ~where:end_;
-         t#scroll_mark_onscreen `INSERT
-       in
-       let iter = t#source_buffer#get_iter `SEL_BOUND in
-       match iter#forward_search text with
-       | None -> 
-           (match t#source_buffer#start_iter#forward_search text with
-           | None -> ()
-           | Some (start,end_) -> highlight start end_)
-       | Some (start,end_) -> highlight start end_
-     in
-     t#source_buffer#insert text;
-     w#toplevel#set_title title;
-     w#scrolledwinContent#add (t :> GObj.widget);
-     ignore(w#entrySearch#connect#activate ~callback);
-     ignore(w#buttonSearch#connect#clicked ~callback);
-     ignore(w#buttonClose#connect#clicked ~callback:(fun () ->
-       w#toplevel#misc#hide (); w#toplevel#destroy ()));
-     w
+
+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
 ;;
+
+