coqide: le undo

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

3 files changed, 148 insertions, 3 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 92a237a7c2..657a0ff1ea 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -106,7 +106,7 @@ module Vector = struct
 end
 
 type 'a viewable_script =
-    {view : GText.view;
+    {view : Undo.undoable_view;
      mutable analyzed_view : 'a option;
     }
 
@@ -116,7 +116,7 @@ object('self)
     val current_all : 'self viewable_script
     val mutable deact_id : GtkSignal.id option
     val input_buffer : GText.buffer
-    val input_view : GText.view
+    val input_view : Undo.undoable_view
     val last_array : string array
     val mutable last_index : bool
     val message_buffer : GText.buffer
@@ -1033,7 +1033,7 @@ let create_input_tab filename =
 	      ~hpolicy:`AUTOMATIC
 	      ~packing:fr1#add () 
   in
-  let tv1 = GText.view ~buffer:b ~packing:(sw1#add) () in
+  let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in
   tv1#misc#set_name "ScriptWindow";
   let _ = tv1#set_editable true in
   let _ = tv1#set_wrap_mode `NONE in
@@ -1345,6 +1345,10 @@ let main files =
   (* Edit Menu *)
   let edit_menu = factory#add_submenu "_Edit" in
   let edit_f = new GMenu.factory edit_menu ~accel_group in
+  ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._z ~callback:
+	   (fun () -> 
+	      ignore (get_current_view()).view#undo));
+  ignore(edit_f#add_separator ());
   ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
 	   (fun () -> GtkSignal.emit_unit
 	      (get_current_view()).view#as_view 
diff --git a/ide/undo.ml b/ide/undo.ml
new file mode 100644
index 0000000000..c05902236b
--- /dev/null
+++ b/ide/undo.ml
@@ -0,0 +1,124 @@
+open GText
+open Ideutils
+type action = 
+  | Insert of string * int * int (* content*pos*length *) 
+  | Delete of string * int * int (* content*pos*length *) 
+
+class undoable_view (tv:Gtk.textview Gtk.obj) =
+  let undo_lock = ref true in 
+object(self)
+  inherit GText.view tv as super
+  val history = (Stack.create () : action Stack.t)
+  val redo = (Queue.create () : action Queue.t)
+
+  method private dump_debug =
+    if !debug then begin
+      prerr_endline "==========Stack top=============";
+      Stack.iter 
+	(fun e -> match e with
+	   | Insert(s,p,l) ->
+ 	       Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
+	   | Delete(s,p,l) -> 			   
+	       Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
+	history;
+      Printf.eprintf "Stack size %d\n" (Stack.length history);
+      prerr_endline "==========Stack Bottom==========";
+      prerr_endline "==========Queue start=============";
+      Queue.iter 
+	(fun e -> match e with
+	   | Insert(s,p,l) ->
+ 	       Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
+	   | Delete(s,p,l) -> 			   
+	       Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
+	redo;
+      Printf.eprintf "Stack size %d\n" (Queue.length redo);
+      prerr_endline "==========Queue End==========" 
+
+    end
+
+  method undo = if !undo_lock then begin
+    undo_lock := false;
+    prerr_endline "UNDO";
+    try begin
+      let r = 
+	match Stack.pop history with
+	  | Insert(s,p,l) as act -> let start = self#buffer#get_iter_at_char p in
+	    (self#buffer#delete_interactive 
+	       ~start
+	       ~stop:(start#forward_chars l)
+	       ()) or
+	    (Stack.push act history; false)
+	  | Delete(s,p,l) as act -> 
+	      let iter = self#buffer#get_iter_at_char p in
+	      (self#buffer#insert_interactive ~iter s) or
+	      (Stack.push act history; false)
+      in if r then begin
+	process_pending ();
+	Queue.push (Stack.pop history) redo
+      end;
+      undo_lock := true; 
+      r
+    end
+    with Stack.Empty -> 
+      undo_lock := true; 
+      false
+  end else
+    (prerr_endline "UNDO DISCARDED"; true)
+
+  method redo = prerr_endline "REDO"; true
+  initializer
+    ignore (self#buffer#connect#insert_text 
+	      ~callback:
+	      (fun it s ->
+		 if !undo_lock && not (Queue.is_empty redo) then begin
+		   Queue.iter (fun e -> Stack.push e history) redo;
+		   Queue.clear redo;
+		 end;
+		   let pos = it#offset in
+		 if Stack.is_empty history or 
+		   s=" " or s="\t" or s="\n" or
+					(match Stack.top history with 
+					   | Insert(old,opos,olen) -> 
+					       opos + olen <> pos
+					   | _ -> true)
+		 then Stack.push (Insert(s,it#offset,Glib.Utf8.length s)) history
+		 else begin
+		   match Stack.pop history with
+		     | Insert(olds,offset,len) -> 
+			 Stack.push 
+			 (Insert(olds^s,
+				 offset,
+				 len+(Glib.Utf8.length s)))
+			 history
+		     | _ -> assert false
+		 end;
+		 self#dump_debug
+	      ));
+    ignore (self#buffer#connect#delete_range
+	      ~callback:
+	      (fun ~start ~stop -> 
+		 if !undo_lock && not (Queue.is_empty redo) then begin
+		   Queue.iter (fun e -> Stack.push e history) redo;
+		   Queue.clear redo;
+		 end;
+		 
+		 Stack.push 
+		   (Delete(self#buffer#get_text ~start ~stop (),
+			   start#offset,
+			   stop#offset - start#offset
+			  ))
+		   history;
+		 self#dump_debug
+	      ))
+end
+
+let undoable_view ?(buffer:buffer option) 
+?editable ?cursor_visible ?wrap_mode
+    ?packing ?show () = 
+    let w = match buffer with 
+      | None -> GtkText.View.create ()
+      | Some b -> GtkText.View.create_with_buffer b#as_buffer
+    in
+    GtkText.View.set w ?editable ?cursor_visible ?wrap_mode;
+    GObj.pack_return (new undoable_view w) ~packing ~show
+
diff --git a/ide/undo.mli b/ide/undo.mli
new file mode 100644
index 0000000000..36700f396f
--- /dev/null
+++ b/ide/undo.mli
@@ -0,0 +1,17 @@
+(* An undoable view class *)
+
+class undoable_view : Gtk.textview Gtk.obj ->
+object
+  inherit GText.view
+  method undo : bool
+  method redo : bool
+end
+
+val undoable_view : 
+  ?buffer:GText.buffer ->
+  ?editable:bool ->
+  ?cursor_visible:bool ->
+  ?wrap_mode:Gtk.Tags.wrap_mode ->
+  ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> undoable_view
+
+