Renamed Undo to conform to CoqIDE widget naming convention. In addition,

made various hack to handle GtkSourceView built-in undo/redo and made
method types and names more compliant with the one of Gtk.

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

5 files changed, 29 insertions, 22 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index c47b301ff4..b5181b0f16 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -63,7 +63,7 @@ end
 
 
 type viewable_script =
-    {script : Undo.undoable_view;
+    {script : Wg_ScriptView.script_view;
      tab_label : GMisc.label;
      proof_view : GText.view;
      message_view : GText.view;
@@ -515,7 +515,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
 let custom_project_files = ref []
 let sup_args = ref []
 
-class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn =
+class analyzed_view (_script:Wg_ScriptView.script_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn =
 object(self)
   val input_view = _script
   val input_buffer = _script#buffer
@@ -1369,7 +1369,7 @@ let create_session file =
       ()
   in
   let script =
-    Undo.undoable_view
+    Wg_ScriptView.script_view
       ~source_buffer:script_buffer
       ~show_line_numbers:true
       ~wrap_mode:`NONE () in
@@ -1638,7 +1638,7 @@ let load_file handler f =
 	prerr_endline "Loading: highlight";
 	input_buffer#set_modified false;
 	prerr_endline "Loading: clear undo";
-	session.script#clear_undo;
+	session.script#clear_undo ();
 	prerr_endline "Loading: success"
       end
   with
@@ -2116,10 +2116,10 @@ let main files =
 	~callback:(fun _ -> do_if_not_computing "undo"
 		     (fun sess ->
 			ignore (sess.analyzed_view#without_auto_complete
-				  (fun () -> session_notebook#current_term.script#undo) ()))
+				  session_notebook#current_term.script#undo ()))
 		     [session_notebook#current_term]) ~stock:`UNDO;
-      GAction.add_action "Clear Undo Stack" ~label:"_Clear Undo Stack"
-	~callback:(fun _ -> ignore session_notebook#current_term.script#clear_undo);
+      GAction.add_action "Redo" ~stock:`REDO
+	~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ()));
       GAction.add_action "Cut" ~callback:(fun _ -> GtkSignal.emit_unit
 					    (get_active_view_for_cp ())
 					    ~sgn:GtkText.View.S.cut_clipboard
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index adfd9e6686..4ba378b7be 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -43,7 +43,7 @@ let init () =
   </menu>
   <menu name='Edit' action='Edit'>
     <menuitem action='Undo' />
-    <menuitem action='Clear Undo Stack' />
+    <menuitem action='Redo' />
     <separator />
     <menuitem action='Cut' />
     <menuitem action='Copy' />
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 5a9a6a8743..c2df9bf47f 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -17,9 +17,9 @@ Preferences
 Project_file
 Ideutils
 Ideproof
+Wg_ScriptView
 Coq_lex
 Gtk_parsing
-Undo
 Coq
 Coq_commands
 Wg_Command
diff --git a/ide/undo.ml b/ide/wg_ScriptView.ml
index 9b33c11e5e..e2801f92ac 100644
--- a/ide/undo.ml
+++ b/ide/wg_ScriptView.ml
@@ -18,7 +18,7 @@ let neg act = match act with
 
 type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
 
-class undoable_view (tv : source_view) =
+class script_view (tv : source_view) =
   let undo_lock = ref true in
 object(self)
   inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
@@ -51,9 +51,12 @@ object(self)
 
     end
 
-  method clear_undo = Stack.clear history; Stack.clear nredo; Queue.clear redo
+  method clear_undo () =
+    Stack.clear history;
+    Stack.clear nredo;
+    Queue.clear redo
 
-  method undo = if !undo_lock then begin
+  method undo () = if !undo_lock then begin
     undo_lock := false;
     prerr_endline "UNDO";
     try begin
@@ -84,7 +87,7 @@ object(self)
   end else
     (prerr_endline "UNDO DISCARDED"; true)
 
-  method redo = prerr_endline "REDO"; true
+  method redo () = prerr_endline "REDO"; true
   initializer
 (* INCORRECT: is called even while undoing...
    ignore (self#buffer#connect#mark_set
@@ -161,10 +164,14 @@ object(self)
 
 		 end*);
 		 self#dump_debug
-	      ))
+	      ));
+    (* Redirect the undo/redo signals of the underlying GtkSourceView *)
+    ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
+    ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));
+
 end
 
-let undoable_view ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spaces =
+let script_view ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spaces =
   GtkSourceView2.SourceView.make_params [] ~cont:(
     GtkText.View.make_params ~cont:(
       GContainer.pack_container ~create:
@@ -175,4 +182,4 @@ let undoable_view ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spac
           let w = Gobject.unsafe_cast w in
 		   Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
 		   Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
-		   ((new undoable_view w) : undoable_view))))
+		   ((new script_view w) : script_view))))
diff --git a/ide/undo.mli b/ide/wg_ScriptView.mli
index b6a59ba756..bc738257cc 100644
--- a/ide/undo.mli
+++ b/ide/wg_ScriptView.mli
@@ -10,15 +10,15 @@
 
 type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
 
-class undoable_view : source_view ->
+class script_view : source_view ->
 object
   inherit GSourceView2.source_view
-  method undo : bool
-  method redo : bool
-  method clear_undo : unit
+  method undo : unit -> bool
+  method redo : unit -> bool
+  method clear_undo : unit -> unit
 end
 
-val undoable_view :
+val script_view :
            ?source_buffer:GSourceView2.source_buffer ->
            ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list ->
            ?auto_indent:bool ->
@@ -41,4 +41,4 @@ val undoable_view :
            ?width:int ->
            ?height:int ->
            ?packing:(GObj.widget -> unit) ->
-           ?show:bool -> unit -> undoable_view
+           ?show:bool -> unit -> script_view