better cb

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index fa0c4a3343b700fa3ace505cf68d5cecac52d361..09a5c3982b3cd4e27b21f71f9a7532ebe3d3d987 100644 (file)
--- a/helm/software/matita/matitaGtkMisc.ml
+++ b/helm/software/matita/matitaGtkMisc.ml
@@ -417,10 +417,7 @@ let new_search_win title text =
      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 callback () = 
        let text = w#entrySearch#text in
        let highlight start end_ =
          t#source_buffer#move_mark `INSERT ~where:start;
@@ -433,7 +430,13 @@ let new_search_win title text =
            (match t#source_buffer#start_iter#forward_search text with
            | None -> ()
            | Some (start,end_) -> highlight start end_)
-       | 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