Wg_Find: regex + case insensitive find/replace support

It uses Str, hence it also supports captures \(..\) and \1 .. \n

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 92 insertions, 202 deletions

diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 319342e91..4b21f27ea 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -8,89 +8,44 @@
 
 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 ~xpad:5
-      ~packing:find_box#pack ()
-  in
-  let find_entry = GEdit.entry
-    ~editable:true
-    ~packing:(find_box#pack ~padding:3 ~expand:true)
-    ()
-  in
-  let next_button =
-    GButton.button
-      ~label:"_Next"
-      ~use_mnemonic:true
-(*       ~stock:`GO_DOWN *)
-      ~packing:(find_box#pack ~padding:3)
-      ()
-  in
-  let previous_button =
-    GButton.button
-      ~label:"_Previous"
-      ~use_mnemonic:true
-(*       ~stock:`GO_UP *)
-      ~packing:(find_box#pack ~padding:3)
-      ()
-  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 ~xpadding:3 ~ypadding:3 ~left:0 ~top:0 ~fill:`X) ()
-  in
-  let _ =
-    GMisc.label ~text:"Replace:"
-      ~xalign:1.0
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:0 ~top:1 ~fill:`X) ()
-  in
-  let r_find_entry = GEdit.entry
-    ~editable:true
-    ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:1 ~top:0 ~expand:`X ~fill:`X)
-    ()
-  in
-  let r_replace_entry = GEdit.entry
-    ~editable:true
-    ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:1 ~top:1 ~expand:`X ~fill:`X)
-    ()
-  in
-  let r_next_button =
-    GButton.button
-      ~label:"_Next" ~use_mnemonic:true
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:0)
-      ()
-  in
-  let r_previous_button =
-    GButton.button
-      ~label:"_Previous" ~use_mnemonic:true
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:0)
-      ()
-  in
-  let r_replace_button =
-    GButton.button
-      ~label:"_Replace" ~use_mnemonic:true
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:2 ~top:1)
-      ()
-  in
-  let r_replace_all_button =
-    GButton.button
-      ~label:"Replace _All" ~use_mnemonic:true
-      ~packing:(replace_box#attach ~xpadding:3 ~ypadding:3 ~left:3 ~top:1)
-      ()
-  in
+class finder name (view : GText.view) =
+  
+  let widget = Wg_Detachable.detachable
+    ~title:(Printf.sprintf "Find & Replace (%s)" name) () in 
+  let replace_box = GPack.table ~columns:4 ~rows:2 ~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
-    val mutable mode : mode = `FIND
 
     method coerce = widget#coerce
 
@@ -100,27 +55,61 @@ class finder (view : GText.view) =
       view#buffer#get_text ~start ~stop ()
 
     method private may_replace () =
-      let search = self#search_text in
-      (search <> "") && (search = self#get_selected_word ())
+      (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#delete_selection () in
-        let _ = view#buffer#insert_interactive r_replace_entry#text in
+        let _ = view#buffer#insert_interactive (self#replacement txt) 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
+      try
+        let i = Str.search_backward regexp text (String.length text - 1) in
+        let j = Str.match_end () in
+        Some(view#buffer#start_iter#forward_chars i,
+             view#buffer#start_iter#forward_chars 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 i, starti#forward_chars j)
+      with Not_found -> None
+
     method replace_all () =
       let rec replace_at (iter : GText.iter) =
-        let found = iter#forward_search self#search_text in
+        let found = self#forward_search iter in
         match found with
         | None -> ()
         | 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 _ = 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 _ = view#buffer#insert_interactive ~iter (self#replacement 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
@@ -130,29 +119,23 @@ class finder (view : GText.view) =
 
     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"]
+      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"]
+      find_entry#misc#modify_base [`NORMAL, `NAME "white"]
 
-    method private find_from backward (starti : GText.iter) text =
+    method private find_from backward (starti : GText.iter) =
       let found =
-        if backward then
-          starti#backward_search text
-        else
-          starti#forward_search text
-      in
+        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 view#buffer#start_iter text
+          self#find_from backward view#buffer#start_iter
         else if backward && not (starti#equal view#buffer#end_iter) then
-          self#find_from backward view#buffer#end_iter text
+          self#find_from backward view#buffer#end_iter
         else
           self#set_not_found ()
       | Some (start, stop) ->
@@ -163,64 +146,30 @@ class finder (view : GText.view) =
 
     method find_forward () =
       let starti = view#buffer#get_iter `SEL_BOUND in
-      self#find_from false starti self#search_text
+      self#find_from false starti
 
     method find_backward () =
       let starti = view#buffer#get_iter `INSERT in
-      self#find_from true starti self#search_text
+      self#find_from true starti
 
-    method private search_text = match mode with
-    | `FIND -> find_entry#text
-    | `REPLACE -> r_find_entry#text
+    method private search_text = find_entry#text
 
     method hide () =
-      widget#misc#hide ();
+      widget#hide;
       view#coerce#misc#grab_focus ()
 
-    method show (mode : mode) = match mode with
-    | `FIND -> self#show_find ()
-    | `REPLACE -> self#show_replace ()
-
-    method private 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 ();
+    method show () =
+      widget#show;
       find_entry#misc#grab_focus ()
 
-    method private 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
 
       (** Widget button interaction *)
       let _ = next_button#connect#clicked ~callback:self#find_forward in
       let _ = previous_button#connect#clicked ~callback:self#find_backward in
-      let _ = r_next_button#connect#clicked ~callback:self#find_forward in
-      let _ = r_previous_button#connect#clicked ~callback:self#find_backward in
-      let _ = r_replace_button#connect#clicked ~callback:self#replace in
-      let _ = r_replace_all_button#connect#clicked ~callback:self#replace_all 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 =
@@ -234,14 +183,13 @@ class finder (view : GText.view) =
       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 find_cb in
-      let _ = r_find_entry#event#connect#key_press replace_cb in
-      let _ = r_replace_entry#event#connect#key_press find_cb in
+      let _ = replace_entry#event#connect#key_press replace_cb in
 
       (** TextView interaction *)
       let view_cb ev =
-        if self#coerce#misc#visible then
+        if widget#visible then
           let ev_key = GdkEvent.Key.keyval ev in
-          if ev_key = GdkKeysyms._Escape then (self#hide (); true)
+          if ev_key = GdkKeysyms._Escape then (widget#hide; true)
           else false
         else false
       in
@@ -249,61 +197,3 @@ class finder (view : GText.view) =
       ()
 
   end
-
-class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.message_view) =
-
-  let widget = GPack.vbox () in
-  (* Search part *)
-  let query_box = GPack.hbox ~packing:widget#add () in
-  let _ =
-    GMisc.label ~text:"Search:"
-      ~xalign:1.0
-      ~packing:query_box#pack ()
-  in
-  let find_entry = GEdit.entry
-    ~editable:true
-    ~packing:(query_box#pack ~expand:true)
-    ()
-  in
-  let next_button =
-    GButton.button
-      ~label:"_Go"
-      ~use_mnemonic:true
-(*       ~stock:`GO_DOWN *)
-      ~packing:query_box#pack
-      ()
-  in
-
-
-  object (self)
-    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 hide () =
-      widget#misc#hide ();
-      view#coerce#misc#grab_focus ()
-
-    method show () =
-      let search =
-        if self#coerce#misc#visible then find_entry#text
-        else
-          self#get_selected_word ()
-      in
-      find_entry#set_text search;
-      widget#misc#show ()
-
-    method private search () =
-      let search = find_entry#text in
-      let len = String.length search in
-      ignore len
-
-    initializer
-      let _ = self#hide () in
-      let _ = next_button#connect#clicked ~callback:self#search in
-      ()
-
-  end