From 4d9e621408101588008761c5aba0033428ae6f5b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jul 2008 10:51:55 +0000 Subject: [PATCH] better cb --- helm/software/matita/matitaGtkMisc.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) 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 -- 2.39.5