From: Enrico Tassi Date: Wed, 13 Jul 2005 12:32:09 +0000 (+0000) Subject: added find&replace facility X-Git-Tag: pre_notation~19 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57b43a967eaf3b0747350cd775d4301a53af2820;p=helm.git added find&replace facility --- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 98526c578..10fb0a1cc 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -881,7 +881,7 @@ Copyright (C) 2005, True - + True gtk-new 1 @@ -902,7 +902,7 @@ Copyright (C) 2005, - + True gtk-open 1 @@ -923,7 +923,7 @@ Copyright (C) 2005, - + True gtk-save 1 @@ -943,7 +943,7 @@ Copyright (C) 2005, True - + True gtk-save-as 1 @@ -970,7 +970,7 @@ Copyright (C) 2005, - + True gtk-quit 1 @@ -992,6 +992,32 @@ Copyright (C) 2005, True _Edit True + + + + + + + True + Find & Replace + True + + + + + True + gtk-find-and-replace + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + @@ -2742,4 +2768,265 @@ Copyright (C) 2005, + + 5 + Find & Replace + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_MOUSE + False + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + + + + True + 3 + 2 + False + 5 + 0 + + + + True + Find: + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + + + 0 + 1 + 0 + 1 + fill + + + + + + + True + Replace with: + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + + + 0 + 1 + 1 + 2 + fill + + + + + + + True + True + True + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 0 + 1 + + + + + + + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 1 + 2 + + + + + + + True + False + 5 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + gtk-find + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-find-and-replace + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Replace + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + 0 + 2 + 2 + 3 + 5 + + + + + + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 0d0fa1ba8..b54dbb777 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -109,6 +109,7 @@ class gui () = let main = new mainWin () in let about = new aboutWin () in let fileSel = new fileSelectionWin () in + let findRepl = new findReplWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in @@ -137,7 +138,7 @@ class gui () = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c fileSel; c main ]); + [ c about; c fileSel; c main; c findRepl]); (* key bindings *) List.iter (* global key bindings *) (fun (key, callback) -> self#addKeyBinding key callback) @@ -156,6 +157,44 @@ class gui () = about#aboutWin#misc#hide ()); about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" ~templ:BuildTimeConf.version about#aboutLabel#label); + (* findRepl win *) + let show_find_Repl () = + findRepl#toplevel#misc#show (); + findRepl#toplevel#misc#grab_focus () + in + let hide_find_Repl () = findRepl#toplevel#misc#hide () in + let find_forward _ = + let highlight start end_ = + source_buffer#move_mark `INSERT ~where:start; + source_buffer#move_mark `SEL_BOUND ~where:end_ + in + let text = findRepl#findEntry#text in + let iter = source_buffer#get_iter `SEL_BOUND in + match iter#forward_search text with + | None -> + (match source_buffer#start_iter#forward_search text with + | None -> () + | Some (start,end_) -> highlight start end_) + | Some (start,end_) -> highlight start end_ + in + let replace _ = + let text = findRepl#replaceEntry#text in + let ins = source_buffer#get_iter `INSERT in + let sel = source_buffer#get_iter `SEL_BOUND in + if ins#compare sel < 0 then + begin + ignore(source_buffer#delete_selection ()); + source_buffer#insert text + end + in + connect_button findRepl#findButton find_forward; + connect_button findRepl#findReplButton replace; + connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ()); + ignore(findRepl#toplevel#event#connect#delete + ~callback:(fun _ -> hide_find_Repl ();true)); + ignore(self#main#findReplMenuItem#connect#activate + ~callback:show_find_Repl); + ignore (findRepl#findEntry#connect#activate ~callback:find_forward); (* file selection win *) ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); ignore (fileSel#fileSelectionWin#connect#response (fun event -> @@ -419,6 +458,7 @@ class gui () = method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) method about = about method fileSel = fileSel + method findRepl = findRepl method main = main method newBrowserWin () = diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 18fe33016..6f9601f71 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -51,6 +51,7 @@ object method about : MatitaGeneratedGui.aboutWin method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin + method findRepl : MatitaGeneratedGui.findReplWin (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console