Back-porting from new Matita:

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

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index fa0c4a3343b700fa3ace505cf68d5cecac52d361..772f17a41643f14250daf5f4c7f60e57d8a99066 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -398,43 +398,26 @@ let utf8_parsed_text s floc =
   let start, stop = HExtlib.loc_of_floc floc in
   let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in
   let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in
-  assert(stop_bytes >= start_bytes);
+  if (stop_bytes < start_bytes) then
+    Printf.sprintf "ERROR (%d > %d)" start_bytes stop_bytes, 0
+  else
   let bytes = stop_bytes - start_bytes in
   try
     String.sub s start_bytes bytes, bytes
   with Invalid_argument _ -> 
-    Printf.eprintf "%s/%d/%d\n" s start_bytes bytes;
-    assert false
-    
+    Printf.sprintf "ERROR (%s/%d/%d)" s start_bytes bytes, 0
   
 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
-     t#source_buffer#insert text;
-     w#toplevel#set_title title;
-     w#scrolledwinContent#add (t :> GObj.widget);
-     ignore(w#buttonSearch#connect#clicked ~callback:( fun () -> 
-       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_));
-     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:"&amp;" 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
 ;;
+
+