1 files changed, 246 insertions, 0 deletions
diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
new file mode 100644
index 0000000000..7e89191bd1
--- /dev/null
+++ b/ide/coqide/wg_Find.ml
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let b2c = Ideutils.byte_offset_to_char_offset
+
+class finder name (view : GText.view) =
+
+  let widget = Wg_Detachable.detachable
+    ~title:(Printf.sprintf "Find & Replace (%s)" name) () in
+  let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
+    ~packing:widget#add () in
+  let hb = GPack.hbox ~packing:(replace_box#attach
+      ~left:1 ~top:0 (*~expand:`X ~fill:`X*)) () in
+  let use_regex =
+    GButton.check_button ~label:"Regular expression"
+      ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
+  let use_nocase =
+    GButton.check_button ~label:"Case insensitive"
+      ~packing:(hb#pack ~expand:false ~fill:true ~padding:3) () in
+  let _ = GMisc.label ~text:"Find:" ~xalign:1.0
+    ~packing:(replace_box#attach
+     (*~xpadding:3 ~ypadding:3*) ~left:0 ~top:1 (*~fill:`X*)) () in
+  let _ = GMisc.label ~text:"Replace:" ~xalign:1.0
+    ~packing:(replace_box#attach
+     (* ~xpadding:3 ~ypadding:3*) ~left:0 ~top:2 (*~fill:`X*)) () in
+  let find_entry = GEdit.entry ~editable:true
+    ~packing:(replace_box#attach
+      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:1 (*~expand:`X ~fill:`X*)) () in
+  let replace_entry = GEdit.entry ~editable:true
+    ~packing:(replace_box#attach
+      (*~xpadding:3 ~ypadding:3*) ~left:1 ~top:2 (*~expand:`X ~fill:`X*)) () in
+  let next_button = GButton.button ~label:"_Next" ~use_mnemonic:true
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:1) () in
+  let previous_button = GButton.button ~label:"_Previous" ~use_mnemonic:true
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:1) () in
+  let replace_button = GButton.button ~label:"_Replace" ~use_mnemonic:true
+    ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:2 ~top:2) () in
+  let replace_all_button =
+    GButton.button ~label:"Replace _All" ~use_mnemonic:true
+      ~packing:(replace_box#attach (*~xpadding:3 ~ypadding:3*) ~left:3 ~top:2) () in
+
+  object (self)
+    val mutable last_found = None
+
+    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 () =
+      (self#search_text <> "") &&
+      (Str.string_match self#regex (self#get_selected_word ()) 0)
+
+    method replace () =
+      if self#may_replace () then
+        let txt = self#get_selected_word () in
+        let () = view#buffer#begin_user_action () in
+        let _ = view#buffer#delete_selection () in
+        let _ = view#buffer#insert_interactive (self#replacement txt) in
+        let () = view#buffer#end_user_action () in
+        self#find_forward ()
+      else self#find_forward ()
+
+    method private regex =
+      let rex = self#search_text in
+      if use_regex#active then
+        if use_nocase#active then Str.regexp_case_fold rex
+        else Str.regexp rex
+      else
+        if use_nocase#active then Str.regexp_string_case_fold rex
+        else Str.regexp_string rex
+
+    method private replacement txt =
+      if use_regex#active then Str.replace_matched replace_entry#text txt
+      else replace_entry#text
+
+    method private backward_search starti =
+      let text = view#buffer#start_iter#get_text ~stop:starti in
+      let regexp = self#regex in
+      let offs = (String.length text - 1) in
+      if offs < 0 then None
+      else try
+        let i = Str.search_backward regexp text offs in
+        let j = Str.match_end () in
+        Some(view#buffer#start_iter#forward_chars (b2c text i),
+             view#buffer#start_iter#forward_chars (b2c text j))
+      with Not_found -> None
+
+    method private forward_search starti =
+      let text = starti#get_text ~stop:view#buffer#end_iter in
+      let regexp = self#regex in
+      try
+        let i = Str.search_forward regexp text 0 in
+        let j = Str.match_end () in
+        Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j))
+      with Not_found -> None
+
+    method replace_all () =
+      let rec replace_at (iter : GText.iter) ct tot =
+        let found = self#forward_search iter in
+        match found with
+        | None ->
+           let tot_str = if Int.equal ct tot then "" else " of " ^ string_of_int tot in
+           let occ_str = CString.plural tot "occurrence" in
+           let _ = Ideutils.flash_info ("Replaced " ^ string_of_int ct ^ tot_str ^ " " ^ occ_str) in
+           ()
+        | Some (start, stop) ->
+          let text = iter#get_text ~stop:view#buffer#end_iter in
+          let start_mark = view#buffer#create_mark start in
+          let stop_mark = view#buffer#create_mark ~left_gravity:false stop in
+          let mod_save = view#buffer#modified in
+          let _ = view#buffer#set_modified false 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 (self#replacement text) in
+          let edited = view#buffer#modified in
+          let _ = view#buffer#set_modified (edited || mod_save) 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
+          let next_ct = if edited then ct + 1 else ct in
+          replace_at next next_ct (tot + 1)
+      in
+      let () = view#buffer#begin_user_action () in
+      let () = replace_at view#buffer#start_iter 0 0 in
+      view#buffer#end_user_action ()
+
+    method private set_not_found () =
+      find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];
+
+    method private set_found () =
+      find_entry#misc#modify_bg [`NORMAL, `NAME "#BAF9CE"]
+
+    method private set_normal () =
+      find_entry#misc#modify_bg [`NORMAL, `NAME "white"]
+
+    method private find_from backward ?(wrapped=false) (starti : GText.iter) =
+      let found =
+        if backward then self#backward_search starti
+        else self#forward_search starti in
+      match found with
+      | None ->
+        if not backward && not (starti#equal view#buffer#start_iter) then
+          self#find_from backward ~wrapped:true view#buffer#start_iter
+        else if backward && not (starti#equal view#buffer#end_iter) then
+          self#find_from backward ~wrapped:true view#buffer#end_iter
+        else
+          let _ = Ideutils.flash_info "String not found" in
+          self#set_not_found ()
+      | Some (start, stop) ->
+        let text = view#buffer#start_iter#get_text ~stop:view#buffer#end_iter in
+        let rec find_all offs accum =
+          if offs > String.length text then
+            List.rev accum
+          else try
+            let i = Str.search_forward self#regex text offs in
+            let j = Str.match_end () in
+            find_all (j + 1) (i :: accum)
+          with Not_found -> List.rev accum
+        in
+        let occurs = find_all 0 [] in
+        let num_occurs = List.length occurs in
+        (* assoc table of offset, occurrence index pairs *)
+        let occur_tbl = List.mapi (fun ndx occ -> (occ,ndx+1)) occurs in
+        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
+        let _ =
+          try
+            let occ_ndx = List.assoc start#offset occur_tbl in
+            let occ_str = CString.plural num_occurs "occurrence" in
+            let wrap_str = if wrapped then
+                             if backward then " (wrapped backwards)"
+                             else " (wrapped)"
+                           else ""
+            in
+            Ideutils.flash_info
+              (string_of_int occ_ndx ^ " of " ^ string_of_int num_occurs ^
+                 " " ^ occ_str ^ wrap_str)
+          with Not_found ->
+            CErrors.anomaly (Pp.str "Occurrence of Find string not in table")
+        in
+        self#set_found ()
+
+    method find_forward () =
+      let starti = view#buffer#get_iter `SEL_BOUND in
+      self#find_from false starti
+
+    method find_backward () =
+      let starti = view#buffer#get_iter `INSERT in
+      self#find_from true starti
+
+    method private search_text = find_entry#text
+
+    method hide () =
+      widget#hide;
+      view#coerce#misc#grab_focus ()
+
+    method show () =
+      widget#show;
+      find_entry#misc#grab_focus ()
+
+    initializer
+      let _ = self#hide () in
+
+      (* Widget button interaction *)
+      let _ = next_button#connect#clicked ~callback:self#find_forward in
+      let _ = previous_button#connect#clicked ~callback:self#find_backward in
+      let _ = replace_button#connect#clicked ~callback:self#replace in
+      let _ = replace_all_button#connect#clicked ~callback:self#replace_all in
+
+      (* Keypress interaction *)
+      let generic_cb esc_cb ret_cb ev =
+        let ev_key = GdkEvent.Key.keyval ev in
+        let (return, _) = GtkData.AccelGroup.parse "Return" in
+        let (esc, _) = GtkData.AccelGroup.parse "Escape" in
+        if ev_key = return then (ret_cb (); true)
+        else if ev_key = esc then (esc_cb (); true)
+        else false
+      in
+      let find_cb = generic_cb self#hide self#find_forward in
+      let replace_cb = generic_cb self#hide self#replace in
+      let _ = find_entry#event#connect#key_press ~callback:find_cb in
+      let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
+
+      (* TextView interaction *)
+      let view_cb ev =
+        if widget#visible then
+          let ev_key = GdkEvent.Key.keyval ev in
+          if ev_key = GdkKeysyms._Escape then (widget#hide; true)
+          else false
+        else false
+      in
+      let _ = view#event#connect#key_press ~callback:view_cb in
+      ()
+
+  end