From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 23 Jul 2008 10:51:55 +0000 (+0000)
Subject: better cb
X-Git-Tag: make_still_working~4887
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d9e621408101588008761c5aba0033428ae6f5b;p=helm.git

better cb
---

diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml
index fa0c4a334..09a5c3982 100644
--- 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