X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGtkMisc.ml;h=872780540197ab9f2f98eaf2c42718606af391cb;hb=56c4e355b88aa505b64c539053aba92eb86afc2a;hp=09a5c3982b3cd4e27b21f71f9a7532ebe3d3d987;hpb=4d9e621408101588008761c5aba0033428ae6f5b;p=helm.git diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index 09a5c3982..872780540 100644 --- 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:"<" text in + let text = Pcre.replace ~pat:"'" ~templ:"'" text in + let text = Pcre.replace ~pat:"\"" ~templ:""" text in + text ;; + +