Added a comment/uncomment command to CoqIDE

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

5 files changed, 91 insertions, 2 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b6c6030e3..27eb5fcea 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1707,6 +1707,7 @@ let main files =
   let navigation_actions = GAction.action_group ~name:"Navigation" () in
   let tactics_actions = GAction.action_group ~name:"Tactics" () in
   let templates_actions = GAction.action_group ~name:"Templates" () in
+  let tools_actions = GAction.action_group ~name:"Tools" () in
   let queries_actions = GAction.action_group ~name:"Queries" () in
   let compile_actions = GAction.action_group ~name:"Compile" () in
   let windows_actions = GAction.action_group ~name:"Windows" () in
@@ -1773,6 +1774,8 @@ let main files =
   let query_shortcut s accel =
     GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s)
   in
+  let comment_f _ = session_notebook#current_term.script#comment () in
+  let uncomment_f _ = session_notebook#current_term.script#uncomment () in
   let add_complex_template (name, label, text, offset, len, key) =
     (* Templates/Lemma *)
     let callback _ =
@@ -1945,7 +1948,7 @@ let main files =
 	 19, 11, Some "T");
       add_complex_template
 	("Definition", "_Definition __", "Definition ident := .\n",
-	 6, 5, Some "D");
+	 6, 5, Some "E");
       add_complex_template
 	("Inductive", "_Inductive __", "Inductive ident : :=\n  | : .\n",
 	 14, 5, Some "I");
@@ -1968,6 +1971,11 @@ let main files =
       query_shortcut "Locate" None;
       query_shortcut "Whelp Locate" None;
     ];
+    GAction.add_actions tools_actions [
+      GAction.add_action "Tools" ~label:"_Tools";
+      GAction.add_action "Comment" ~label:"_Comment" ~callback:comment_f ~accel:"<CTRL>D";
+      GAction.add_action "Uncomment" ~label:"_Uncomment" ~callback:uncomment_f ~accel:"<CTRL><SHIFT>D";
+    ];
     GAction.add_actions compile_actions [
       GAction.add_action "Compile" ~label:"_Compile";
       GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f;
@@ -2029,6 +2037,7 @@ let main files =
     Coqide_ui.ui_m#insert_action_group navigation_actions 0;
     Coqide_ui.ui_m#insert_action_group tactics_actions 0;
     Coqide_ui.ui_m#insert_action_group templates_actions 0;
+    Coqide_ui.ui_m#insert_action_group tools_actions 0;
     Coqide_ui.ui_m#insert_action_group queries_actions 0;
     Coqide_ui.ui_m#insert_action_group compile_actions 0;
     Coqide_ui.ui_m#insert_action_group windows_actions 0;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 04e1e488d..6041edff7 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -118,6 +118,10 @@ let init () =
     <menuitem action='Locate' />
     <menuitem action='Whelp Locate' />
   </menu>
+  <menu name='Tools' action='Tools'>
+    <menuitem action='Comment' />
+    <menuitem action='Uncomment' />
+  </menu>
   <menu action='Compile'>
     <menuitem action='Compile buffer' />
     <menuitem action='Make' />
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 21369d6f6..a04c2278c 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -272,7 +272,7 @@ class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.
     method private search () =
       let search = find_entry#text in
       let len = String.length search in
-      ()
+      ignore len
 
     initializer
       let _ = self#hide () in
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 57752de4f..2c524ab74 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -254,6 +254,80 @@ object (self)
     } in
     Gobject.set prop obj show
 
+  method comment () =
+    let rec get_line_start iter =
+      if iter#starts_line then iter
+      else get_line_start iter#backward_char
+    in
+    let (start, stop) =
+      if self#buffer#has_selection then
+        self#buffer#selection_bounds
+      else
+        let insert = self#buffer#get_iter `INSERT in
+        (get_line_start insert, insert#forward_to_line_end)
+    in
+      let stop_mark = self#buffer#create_mark ~left_gravity:false stop in
+      let () = self#buffer#begin_user_action () in
+      let was_inserted = self#buffer#insert_interactive ~iter:start "(* " in
+      let stop = self#buffer#get_iter_at_mark (`MARK stop_mark) in
+      let () = if was_inserted then ignore (self#buffer#insert_interactive ~iter:stop " *)") in
+      let () = self#buffer#end_user_action () in
+      self#buffer#delete_mark (`MARK stop_mark)
+
+  method uncomment () =
+    let rec get_left_iter depth (iter : GText.iter) =
+      let prev_close = iter#backward_search "*)" in
+      let prev_open = iter#backward_search "(*" in
+      let prev_object = match prev_close, prev_open with
+      | None, None | Some _, None -> `NONE
+      | None, Some (po, _) -> `OPEN po
+      | Some (co, _), Some (po, _) -> if co#compare po < 0 then `OPEN po else `CLOSE co
+      in
+      match prev_object with
+      | `NONE -> None
+      | `OPEN po ->
+        if depth <= 0 then Some po
+        else get_left_iter (pred depth) po
+      | `CLOSE co ->
+        get_left_iter (succ depth) co
+    in
+    let rec get_right_iter depth (iter : GText.iter) =
+      let next_close = iter#forward_search "*)" in
+      let next_open = iter#forward_search "(*" in
+      let next_object = match next_close, next_open with
+      | None, None | None, Some _ -> `NONE
+      | Some (_, co), None -> `CLOSE co
+      | Some (_, co), Some (_, po) ->
+        if co#compare po > 0 then `OPEN po else `CLOSE co
+      in
+      match next_object with
+      | `NONE -> None
+      | `OPEN po ->
+        get_right_iter (succ depth) po
+      | `CLOSE co ->
+        if depth <= 0 then Some co
+        else get_right_iter (pred depth) co
+    in
+    let insert = self#buffer#get_iter `INSERT in
+    let left_elt = get_left_iter 0 insert in
+    let right_elt = get_right_iter 0 insert in
+    match left_elt, right_elt with
+    | Some liter, Some riter ->
+      let stop_mark = self#buffer#create_mark ~left_gravity:false riter in
+      (* We remove one trailing/leading space if it exists *)
+      let lcontent = self#buffer#get_text ~start:liter ~stop:(liter#forward_chars 3) () in
+      let rcontent = self#buffer#get_text ~start:(riter#backward_chars 3) ~stop:riter () in
+      let llen = if lcontent = "(* " then 3 else 2 in
+      let rlen = if rcontent = " *)" then 3 else 2 in
+      (* Atomic operation for the user *)
+      let () = self#buffer#begin_user_action () in
+      let was_deleted = self#buffer#delete_interactive ~start:liter ~stop:(liter#forward_chars llen) () in
+      let riter = self#buffer#get_iter_at_mark (`MARK stop_mark) in
+      if was_deleted then ignore (self#buffer#delete_interactive ~start:(riter#backward_chars rlen) ~stop:riter ());
+      let () = self#buffer#end_user_action () in
+      self#buffer#delete_mark (`MARK stop_mark)
+    | _ -> ()
+
   initializer
     (* Install undo managing *)
     ignore (self#buffer#connect#insert_text ~callback:self#handle_insert);
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index 8dc951e7d..e94ce4904 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -22,6 +22,8 @@ object
   method set_right_margin_position : int -> unit
   method show_right_margin : bool
   method set_show_right_margin : bool -> unit
+  method comment : unit -> unit
+  method uncomment : unit -> unit
 end
 
 val script_view : Coq.coqtop ->