diff options
| -rw-r--r-- | ide/coqide.ml | 378 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 7 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/mac_default_accel_map | 4 | ||||
| -rw-r--r-- | ide/tags.ml | 1 | ||||
| -rw-r--r-- | ide/tags.mli | 1 | ||||
| -rw-r--r-- | ide/wg_Find.ml | 319 | ||||
| -rw-r--r-- | ide/wg_Find.mli | 19 |
8 files changed, 368 insertions, 362 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 9540fe4b9..78f98e889 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -103,6 +103,7 @@ type viewable_script = analyzed_view : analyzed_views; toplvl : Coq.coqtop ref; command : Wg_Command.command_window; + finder : Wg_Find.finder; } let kill_session s = @@ -111,8 +112,11 @@ let kill_session s = let build_session s = let session_paned = GPack.paned `VERTICAL () in + let session_box = + GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) () + in let eval_paned = GPack.paned `HORIZONTAL ~border_width:5 - ~packing:(session_paned#pack1 ~shrink:false ~resize:true) () in + ~packing:(session_box#pack ~expand:true) () in let script_frame = GBin.frame ~shadow_type:`IN ~packing:eval_paned#add1 () in let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC @@ -148,6 +152,7 @@ let build_session s = old_paned_height := paned_height; ))) in + session_box#pack s.finder#coerce; session_paned#pack2 ~shrink:false ~resize:false (s.command#frame#coerce); script_scroll#add s.script#coerce; proof_scroll#add s.proof_view#coerce; @@ -594,7 +599,6 @@ object(self) val mutable last_modification_time = 0. val mutable last_auto_save_time = 0. val mutable detached_views = [] - val mutable find_forward_instead_of_backward = false val mutable auto_complete_on = !current.auto_complete val hidden_proofs = Hashtbl.create 32 @@ -1513,6 +1517,7 @@ let create_session file = in let ct = ref (Coq.spawn_coqtop coqtop_args) in let command = new Wg_Command.command_window ct current in + let finder = new Wg_Find.finder (script :> GText.view) in let legacy_av = new analyzed_view script proof message stack ct file in let () = legacy_av#update_stats in let _ = @@ -1562,7 +1567,8 @@ let create_session file = analyzed_view=legacy_av; encoding=""; toplvl=ct; - command=command + command=command; + finder=finder; } (* XXX - to be used later @@ -1966,214 +1972,6 @@ let main files = | Some av -> av#set_auto_complete b | None -> ()); *) - -(* begin of find/replace mechanism *) - let last_found = ref None in - let search_backward = ref false in - let find_w = GWindow.window - (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *) - (* ~allow_grow:true ~allow_shrink:true *) - (* ~width:!current.window_width ~height:!current.window_height *) - ~position:`CENTER - ~title:"CoqIde search/replace" () - in - let find_box = GPack.table - ~columns:3 ~rows:5 - ~col_spacings:10 ~row_spacings:10 ~border_width:10 - ~homogeneous:false ~packing:find_w#add () in - - let _ = - GMisc.label ~text:"Find:" - ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () - in - let find_entry = GEdit.entry - ~editable: true - ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X) - () - in - let _ = - GMisc.label ~text:"Replace with:" - ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () - in - let replace_entry = GEdit.entry - ~editable: true - ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X) - () - in - (* let _ = - GButton.check_button - ~label:"case sensitive" - ~active:true - ~packing: (find_box#attach ~left:1 ~top:2) - () - in - *) - let find_backwards_check = - GButton.check_button - ~label:"search backwards" - ~active:!search_backward - ~packing: (find_box#attach ~left:1 ~top:3) - () - in - let close_find_button = - GButton.button - ~label:"Close" - ~packing: (find_box#attach ~left:2 ~top:2) - () - in - let replace_find_button = - GButton.button - ~label:"Replace and find" - ~packing: (find_box#attach ~left:2 ~top:1) - () - in - let find_again_button = - GButton.button - ~label:"_Find again" - ~packing: (find_box#attach ~left:2 ~top:0) - () - in - let last_find () = - let v = session_notebook#current_term.script in - let b = v#buffer in - let start,stop = - match !last_found with - | None -> let i = b#get_iter_at_mark `INSERT in (i,i) - | Some(start,stop) -> - let start = b#get_iter_at_mark start - and stop = b#get_iter_at_mark stop - in - b#remove_tag Tags.Script.found ~start ~stop; - last_found:=None; - start,stop - in - (v,b,start,stop) - in - let do_replace () = - let v = session_notebook#current_term.script in - let b = v#buffer in - match !last_found with - | None -> () - | Some(start,stop) -> - let start = b#get_iter_at_mark start - and stop = b#get_iter_at_mark stop - in - b#delete ~start ~stop; - b#insert ~iter:start replace_entry#text; - last_found:=None - in - let find_from (v : Undo.undoable_view) - (b : GText.buffer) (starti : GText.iter) text = - prerr_endline ("Searching for " ^ text); - match (if !search_backward then starti#backward_search text - else starti#forward_search text) - with - | None -> () - | Some(start,stop) -> - b#apply_tag Tags.Script.found ~start ~stop; - let start = `MARK (b#create_mark start) - and stop = `MARK (b#create_mark stop) - in - v#scroll_to_mark ~use_align:false ~yalign:0.75 ~within_margin:0.25 - stop; - last_found := Some(start,stop) - in - let do_find () = - let (v,b,starti,_) = last_find () in - find_from v b starti find_entry#text - in - let do_replace_find () = - do_replace(); - do_find() - in - let close_find () = - let (v,b,_,stop) = last_find () in - b#place_cursor ~where:stop; - find_w#misc#hide(); - v#coerce#misc#grab_focus() - in - to_do_on_page_switch := - (fun i -> if find_w#misc#visible then close_find()):: - !to_do_on_page_switch; - let find_again () = - let (v,b,start,_) = last_find () in - let start = - if !search_backward - then start#backward_chars 1 - else start#forward_chars 1 - in - find_from v b start find_entry#text - in - let click_on_backward () = - search_backward := not !search_backward - in - let key_find ev = - let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in - if k = GdkKeysyms._Escape then - begin - let (v,b,_,stop) = last_find () in - find_w#misc#hide(); - v#coerce#misc#grab_focus(); - true - end - else if k = GdkKeysyms._Escape then - begin - close_find(); - true - end - else if k = GdkKeysyms._Return || - List.mem `CONTROL s && k = GdkKeysyms._f then - begin - find_again (); - true - end - else if List.mem `CONTROL s && k = GdkKeysyms._b then - begin - find_backwards_check#set_active (not !search_backward); - true - end - else false (* to let default callback execute *) - in - let find_f ~backward () = - let save_dir = !search_backward in - search_backward := backward; - find_w#show (); - find_w#present (); - find_entry#misc#grab_focus (); - search_backward := save_dir - in - let _ = find_again_button#connect#clicked find_again in - let _ = close_find_button#connect#clicked close_find in - let _ = replace_find_button#connect#clicked do_replace_find in - let _ = find_backwards_check#connect#clicked click_on_backward in - let _ = find_entry#connect#changed do_find in - let _ = find_entry#event#connect#key_press ~callback:key_find in - let _ = find_w#event#connect#delete ~callback:(fun _ -> find_w#misc#hide(); true) in - (* - let search_if = edit_f#add_item "Search _forward" - ~key:GdkKeysyms._greater - in - let search_ib = edit_f#add_item "Search _backward" - ~key:GdkKeysyms._less - in - *) - (* - let complete_i = edit_f#add_item "_Complete" - ~key:GdkKeysyms._comma - ~callback: - (do_if_not_computing - (fun b -> - let v = session_notebook#current_term.analyzed_view - - in v#complete_at_offset - ((v#view#buffer#get_iter `SEL_BOUND)#offset) - )) - in - complete_i#misc#set_state `INSENSITIVE; - *) -(* end of find/replace mechanism *) (* begin Preferences *) let reset_revert_timer () = disconnect_revert_timer (); @@ -2458,8 +2256,16 @@ let main files = session_notebook#current_term.script#as_view ~sgn:GtkText.View.S.paste_clipboard with _ -> prerr_endline "EMIT PASTE FAILED") ~stock:`PASTE; - GAction.add_action "Find in buffer" ~label:"_Find in buffer" ~callback:(fun _ -> find_f ~backward:false ()) ~stock:`FIND; - GAction.add_action "Find backwards" ~label:"Find _backwards" ~callback:(fun _ -> find_f ~backward:true ()) ~accel:"<Ctrl>b"; + GAction.add_action "Find" ~label:"_Find" ~stock:`FIND ~accel:"<Ctrl>F" + ~callback:(fun _ -> session_notebook#current_term.finder#show_find ()); + GAction.add_action "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3" + ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ()); + GAction.add_action "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"<Shift>F3" + ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ()); + GAction.add_action "Replace" ~label:"_Replace" ~stock:`FIND_AND_REPLACE ~accel:"<Ctrl>R" + ~callback:(fun _ -> session_notebook#current_term.finder#show_replace ()); + GAction.add_action "Close Find" ~accel:"Escape" + ~callback:(fun _ -> session_notebook#current_term.finder#hide ()); GAction.add_action "Complete Word" ~label:"Complete Word" ~callback:(fun _ -> ignore ( let av = session_notebook#current_term.analyzed_view in @@ -2496,7 +2302,7 @@ let main files = if ccw#frame#misc#visible then ccw#frame#misc#hide () else ccw#frame#misc#show ()) - ~accel:"Escape"; + ~accel:"<Alt>Escape"; ]; List.iter (fun (opts,name,label,key,dflt) -> @@ -2670,150 +2476,6 @@ let main files = let nb = session_notebook in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in lower_hbox#pack ~expand:true status#coerce; - let search_lbl = GMisc.label ~text:"Search:" - ~show:false - ~packing:(lower_hbox#pack ~expand:false) () - in - let search_history = ref [] in - let (search_input,_) = GEdit.combo_box_entry_text ~strings:!search_history ~show:false - ~packing:(lower_hbox#pack ~expand:false) () - in - let ready_to_wrap_search = ref false in - - let start_of_search = ref None in - let start_of_found = ref None in - let end_of_found = ref None in - let search_forward = ref true in - let matched_word = ref None in - - let memo_search () = - matched_word := Some search_input#entry#text - in - let end_search () = - prerr_endline "End Search"; - memo_search (); - let v = session_notebook#current_term.script in - v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT); - v#coerce#misc#grab_focus (); - search_input#entry#set_text ""; - search_lbl#misc#hide (); - search_input#misc#hide () - in - let end_search_focus_out () = - prerr_endline "End Search(focus out)"; - memo_search (); - let v = session_notebook#current_term.script in - v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT); - search_input#entry#set_text ""; - search_lbl#misc#hide (); - search_input#misc#hide () - in - ignore (search_input#entry#connect#activate ~callback:end_search); - ignore (search_input#entry#event#connect#key_press - ~callback:(fun k -> let kv = GdkEvent.Key.keyval k in - if - kv = GdkKeysyms._Right - || kv = GdkKeysyms._Up - || kv = GdkKeysyms._Left - || (kv = GdkKeysyms._g - && (List.mem `CONTROL (GdkEvent.Key.state k))) - then end_search (); - false)); - ignore (search_input#entry#event#connect#focus_out - ~callback:(fun _ -> end_search_focus_out (); false)); - to_do_on_page_switch := - (fun i -> - start_of_search := None; - ready_to_wrap_search:=false)::!to_do_on_page_switch; - - (* TODO : make it work !!! *) - let rec search_f () = - search_lbl#misc#show (); - search_input#misc#show (); - - prerr_endline "search_f called"; - if !start_of_search = None then begin - (* A full new search is starting *) - start_of_search := - Some (session_notebook#current_term.script#buffer#create_mark - (session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT)); - start_of_found := !start_of_search; - end_of_found := !start_of_search; - matched_word := Some ""; - end; - let txt = search_input#entry#text in - let v = session_notebook#current_term.script in - let iit = v#buffer#get_iter_at_mark `SEL_BOUND - and insert_iter = v#buffer#get_iter_at_mark `INSERT - in - prerr_endline ("SELBOUND="^(string_of_int iit#offset)); - prerr_endline ("INSERT="^(string_of_int insert_iter#offset)); - - (match - if !search_forward then iit#forward_search txt - else let npi = iit#forward_chars (Glib.Utf8.length txt) in - match - (npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset), - (let t = iit#get_text ~stop:npi in - flash_info (t^"\n"^txt); - t = txt) - with - | true,true -> - (flash_info "T,T";iit#backward_search txt) - | false,true -> flash_info "F,T";Some (iit,npi) - | _,false -> - (iit#backward_search txt) - - with - | None -> - if !ready_to_wrap_search then begin - ready_to_wrap_search := false; - flash_info "Search wrapped"; - v#buffer#place_cursor - ~where:(if !search_forward then v#buffer#start_iter else - v#buffer#end_iter); - search_f () - end else begin - if !search_forward then flash_info "Search at end" - else flash_info "Search at start"; - ready_to_wrap_search := true - end - | Some (start,stop) -> - prerr_endline "search: before moving marks"; - prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset)); - prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset)); - - v#buffer#move_mark `SEL_BOUND ~where:start; - v#buffer#move_mark `INSERT ~where:stop; - prerr_endline "search: after moving marks"; - prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset)); - prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset)); - v#scroll_to_mark `SEL_BOUND - ) - in - ignore (search_input#entry#event#connect#key_release - ~callback: - (fun ev -> - if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin - let v = session_notebook#current_term.script in - (match !start_of_search with - | None -> - prerr_endline "search_key_rel: Placing sel_bound"; - v#buffer#move_mark - `SEL_BOUND - ~where:(v#buffer#get_iter_at_mark `INSERT) - | Some mk -> let it = v#buffer#get_iter_at_mark - (`MARK mk) in - prerr_endline "search_key_rel: Placing cursor"; - v#buffer#place_cursor ~where:it; - start_of_search := None - ); - search_input#entry#set_text ""; - v#coerce#misc#grab_focus (); - end; - false - )); - ignore (search_input#entry#connect#changed ~callback:search_f); push_info "Ready"; (* Location display *) let l = GMisc.label diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index eaf1e9348..6b464348c 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -20,6 +20,7 @@ let list_items menu li = let init () = let theui = Printf.sprintf "<ui> +<accelerator action='Close Find' /> <menubar name='CoqIde MenuBar'> <menu action='File'> <menuitem action='New' /> @@ -48,8 +49,10 @@ let init () = <menuitem action='Copy' /> <menuitem action='Paste' /> <separator /> - <menuitem action='Find in buffer' /> - <menuitem action='Find backwards' /> + <menuitem action='Find' /> + <menuitem action='Find Next' /> + <menuitem action='Find Previous' /> + <menuitem action='Replace' /> <menuitem action='Complete Word' /> <separator /> <menuitem action='External editor' /> diff --git a/ide/ide.mllib b/ide/ide.mllib index ee498ba0c..5a9a6a874 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -10,6 +10,7 @@ Editable_cells Config_parser Tags Wg_Notebook +Wg_Find Config_lexer Utf8_convert Preferences diff --git a/ide/mac_default_accel_map b/ide/mac_default_accel_map index 4d34636f4..e570ae651 100644 --- a/ide/mac_default_accel_map +++ b/ide/mac_default_accel_map @@ -108,7 +108,7 @@ ; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose sum/" "") ; (gtk_accel_path "<DEFAULT ROOT>/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "") ; (gtk_accel_path "<CoqIde MenuBar>/Te_mplates/" "") -(gtk_accel_path "<Actions>/Edit/Find in buffer" "<Meta>f") +(gtk_accel_path "<Actions>/Edit/Find" "<Meta>f") ; (gtk_accel_path "<DEFAULT ROOT>/r_eplace __ with/" "") (gtk_accel_path "<Actions>/Tactics/omega" "<Meta><Control>o") ; (gtk_accel_path "<DEFAULT ROOT>/S_cheme/" "") @@ -308,7 +308,7 @@ ; (gtk_accel_path "<CoqIde MenuBar>/Templates/_U.../" "") (gtk_accel_path "<Actions>/Display/Display raw matching expressions" "<Shift><Control>m") ; (gtk_accel_path "<DEFAULT ROOT>/c_asetype/" "") -(gtk_accel_path "<Actions>/Edit/Find backwards" "<Meta>b") +(gtk_accel_path "<Actions>/Edit/Find Previous" "<Meta>b") ; (gtk_accel_path "<DEFAULT ROOT>/S_ave./" "") ; (gtk_accel_path "<DEFAULT ROOT>/p_attern/" "") ; (gtk_accel_path "<DEFAULT ROOT>/M_odule/" "") diff --git a/ide/tags.ml b/ide/tags.ml index eeace4658..73da20f21 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -34,6 +34,7 @@ struct let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"] let sentence = make_tag table ~name:"sentence" [] + let replaced = make_tag table ~name:"replaced" [`BACKGROUND "green"] end module Proof = struct diff --git a/ide/tags.mli b/ide/tags.mli index 53a8c4930..4dc0b9fc8 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -24,6 +24,7 @@ sig val folded : GText.tag val paren : GText.tag val sentence : GText.tag + val replaced : GText.tag end module Proof : diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml new file mode 100644 index 000000000..0bd1f6e06 --- /dev/null +++ b/ide/wg_Find.ml @@ -0,0 +1,319 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type mode = +| Find +| Replace + +class finder (view : GText.view) = + + let widget = GPack.vbox () in + (* Find part *) + let find_box = GPack.hbox ~packing:widget#add () in + let _ = + GMisc.label ~text:"Find:" + ~xalign:1.0 + ~packing:find_box#pack () + in + let find_entry = GEdit.entry + ~editable:true + ~packing:(find_box#pack ~expand:true) + () + in + let next_button = + GButton.button + ~label:"_Next" + ~use_mnemonic:true +(* ~stock:`GO_DOWN *) + ~packing:find_box#pack + () + in + let previous_button = + GButton.button + ~label:"_Previous" + ~use_mnemonic:true +(* ~stock:`GO_UP *) + ~packing:find_box#pack + () + in + (* Find and replace part *) + let replace_box = GPack.table + ~columns:4 ~rows:2 + ~homogeneous:false ~packing:widget#add () in + let _ = + GMisc.label ~text:"Find:" + ~xalign:1.0 + ~packing:(replace_box#attach ~left:0 ~top:0 ~fill:`X) () + in + let _ = + GMisc.label ~text:"Replace:" + ~xalign:1.0 + ~packing:(replace_box#attach ~left:0 ~top:1 ~fill:`X) () + in + let r_find_entry = GEdit.entry + ~editable:true + ~packing:(replace_box#attach ~left:1 ~top:0 ~expand:`X ~fill:`X) + () + in + let r_replace_entry = GEdit.entry + ~editable:true + ~packing:(replace_box#attach ~left:1 ~top:1 ~expand:`X ~fill:`X) + () + in + let r_next_button = + GButton.button + ~label:"_Next" ~use_mnemonic:true + ~packing:(replace_box#attach ~left:2 ~top:0) + () + in + let r_previous_button = + GButton.button + ~label:"_Previous" ~use_mnemonic:true + ~packing:(replace_box#attach ~left:3 ~top:0) + () + in + let r_replace_button = + GButton.button + ~label:"_Replace" ~use_mnemonic:true + ~packing:(replace_box#attach ~left:2 ~top:1) + () + in + let r_replace_all_button = + GButton.button + ~label:"Replace _All" ~use_mnemonic:true + ~packing:(replace_box#attach ~left:3 ~top:1) + () + in + + object (self) + val mutable last_found = None + val mutable mode = Find + + method coerce = widget#coerce + + method private get_selected_word () = + let start = view#buffer#get_iter `INSERT in + let stop = view#buffer#get_iter `SEL_BOUND in + view#buffer#get_text ~start ~stop () + + method private may_replace () = + let search = self#search_text in + (search <> "") && (search = self#get_selected_word ()) + + method replace () = + if self#may_replace () then + let _ = view#buffer#delete_selection () in + let _ = view#buffer#insert_interactive r_replace_entry#text in + self#find_forward () + else self#find_forward () + + method replace_all () = + let rec replace_at (iter : GText.iter) = + let found = iter#forward_search self#search_text in + match found with + | None -> () + | Some (start, stop) -> + let () = Printf.printf "%i-%i\n%!" start#offset stop#offset in + let start_mark = view#buffer#create_mark start in + let stop_mark = view#buffer#create_mark stop in + let _ = view#buffer#delete_interactive ~start ~stop () in + let iter = view#buffer#get_iter_at_mark (`MARK start_mark) in + let _ = view#buffer#insert_interactive ~iter r_replace_entry#text in + let next = view#buffer#get_iter_at_mark (`MARK stop_mark) in + let () = view#buffer#delete_mark (`MARK start_mark) in + let () = view#buffer#delete_mark (`MARK stop_mark) in + replace_at next + in + replace_at view#buffer#start_iter + + method private set_not_found () = + find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"]; + r_find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"]; + + method private set_found () = + find_entry#misc#modify_base [`NORMAL, `NAME "#BAF9CE"]; + r_find_entry#misc#modify_base [`NORMAL, `NAME "#BAF9CE"] + + method private set_normal () = + find_entry#misc#modify_base [`NORMAL, `NAME "white"]; + r_find_entry#misc#modify_base [`NORMAL, `NAME "white"] + + method private find_from backward (starti : GText.iter) text = + let found = + if backward then + starti#backward_search text + else + starti#forward_search text + in + match found with + | None -> + if not backward && not (starti#equal view#buffer#start_iter) then + self#find_from backward view#buffer#start_iter text + else if backward && not (starti#equal view#buffer#end_iter) then + self#find_from backward view#buffer#end_iter text + else + self#set_not_found () + | Some (start, stop) -> + let _ = view#buffer#select_range start stop in + let scroll = `MARK (view#buffer#create_mark stop) in + let _ = view#scroll_to_mark ~use_align:false scroll in + self#set_found () + + method find_forward () = + let starti = view#buffer#get_iter `SEL_BOUND in + self#find_from false starti self#search_text + + method find_backward () = + let starti = view#buffer#get_iter `INSERT in + self#find_from true starti self#search_text + + method private search_text = match mode with + | Find -> find_entry#text + | Replace -> r_find_entry#text + + method hide () = + widget#misc#hide (); + view#coerce#misc#grab_focus () + + method show_find () = + mode <- Find; + let search = + if self#coerce#misc#visible then + r_find_entry#text + else + self#get_selected_word () + in + self#set_normal (); + find_entry#set_text search; + widget#misc#show (); + find_box#misc#show (); + replace_box#misc#hide (); + find_entry#misc#grab_focus () + + method show_replace () = + mode <- Replace; + let search = + if self#coerce#misc#visible then + find_entry#text + else + self#get_selected_word () + in + self#set_normal (); + r_find_entry#set_text search; + widget#misc#show (); + find_box#misc#hide (); + replace_box#misc#show (); + r_find_entry#misc#grab_focus () + + initializer + let _ = self#hide () in + let _ = next_button#connect#clicked self#find_forward in + let _ = previous_button#connect#clicked self#find_backward in + let _ = r_next_button#connect#clicked self#find_forward in + let _ = r_previous_button#connect#clicked self#find_backward in + let _ = r_replace_button#connect#clicked self#replace in + let _ = r_replace_all_button#connect#clicked self#replace_all in +(* let insert_cb _ ~pos = self#find_forward () in + let delete_cb ~start ~stop = self#find_backward () in*) +(* let _ = find_entry#connect#insert_text ~callback:insert_cb in + let _ = find_entry#connect#delete_text ~callback:delete_cb in*) +(* let _ = find_again_button#connect#clicked find_again in *) +(* let _ = close_find_button#connect#clicked close_find in *) +(* let _ = replace_find_button#connect#clicked do_replace_find in *) +(* let _ = find_backwards_check#connect#clicked click_on_backward in *) +(* let _ = find_entry#connect#changed do_find in *) + () + + end + +(* let find_box = GPack.table + ~columns:3 ~rows:5 + ~col_spacings:10 ~row_spacings:10 ~border_width:10 + ~homogeneous:false ~packing:find_w#add () in + +let _ = + GMisc.label ~text:"Find:" + ~xalign:1.0 + ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () +in +let _ = + GMisc.label ~text:"Replace with:" + ~xalign:1.0 + ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () +in *) +(* let _ = + GButton.check_button + ~label:"case sensitive" + ~active:true + ~packing: (find_box#attach ~left:1 ~top:2) + () + in +*) +(* let find_backwards_check = + GButton.check_button + ~label:"search backwards" + ~active:!search_backward + ~packing: (find_box#attach ~left:1 ~top:3) + () +in +let close_find_button = + GButton.button + ~label:"Close" + ~packing: (find_box#attach ~left:2 ~top:2) + () +in +let replace_find_button = + GButton.button + ~label:"Replace and find" + ~packing: (find_box#attach ~left:2 ~top:1) + () +in +let find_again_button = + GButton.button + ~label:"_Find again" + ~packing: (find_box#attach ~left:2 ~top:0) + () +in*) + +(*let key_find ev = + let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in + if k = GdkKeysyms._Escape then + begin + let (v,b,_,stop) = last_find () in + find_w#misc#hide(); + v#coerce#misc#grab_focus(); + true + end + else if k = GdkKeysyms._Escape then + begin + close_find(); + true + end + else if k = GdkKeysyms._Return || + List.mem `CONTROL s && k = GdkKeysyms._f then + begin + find_again (); + true + end + else if List.mem `CONTROL s && k = GdkKeysyms._b then + begin + find_backwards_check#set_active (not !search_backward); + true + end + else false (* to let default callback execute *) + +in *) + +(* let find_f ~backward () = + let save_dir = !search_backward in + search_backward := backward; + find_w#show (); + find_w#present (); + find_entry#misc#grab_focus (); + search_backward := save_dir +*)
\ No newline at end of file diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli new file mode 100644 index 000000000..96025e188 --- /dev/null +++ b/ide/wg_Find.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +class finder : GText.view -> + object + method coerce : GObj.widget + method hide : unit -> unit + method show_find : unit -> unit + method show_replace : unit -> unit + method replace : unit -> unit + method replace_all : unit -> unit + method find_backward : unit -> unit + method find_forward : unit -> unit + end |