better UI for TeX/Unicode and terms grammar

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

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index 9c00dfddef4aa1b7879026c85e12fa1df0c3700d..fa0c4a3343b700fa3ace505cf68d5cecac52d361 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -412,3 +412,29 @@ let utf8_string_length s =
     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
+;;