diff options
Diffstat (limited to 'ide/undo.ml')
| -rw-r--r-- | ide/undo.ml | 178 |
1 files changed, 178 insertions, 0 deletions
diff --git a/ide/undo.ml b/ide/undo.ml new file mode 100644 index 00000000..54449515 --- /dev/null +++ b/ide/undo.ml @@ -0,0 +1,178 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: undo.ml,v 1.8.2.1 2004/07/16 19:30:21 herbelin Exp $ *) + +open GText +open Ideutils +type action = + | Insert of string * int * int (* content*pos*length *) + | Delete of string * int * int (* content*pos*length *) + +let neg act = match act with + | Insert (s,i,l) -> Delete (s,i,l) + | Delete (s,i,l) -> Insert (s,i,l) + +class undoable_view (tv:Gtk.text_view 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) + val nredo = (Stack.create () : action Stack.t) + + method private dump_debug = + if false (* !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 clear_undo = Stack.clear history; Stack.clear nredo; Queue.clear redo + + 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 (); + let act = Stack.pop history in + Queue.push act redo; + Stack.push act nredo + 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 +(* INCORRECT: is called even while undoing... + ignore (self#buffer#connect#mark_set + ~callback: + (fun it tm -> if !undo_lock && not (Queue.is_empty redo) then begin + Stack.iter (fun e -> Stack.push (neg e) history) nredo; + Stack.clear nredo; + Queue.iter (fun e -> Stack.push e history) redo; + Queue.clear redo; + end) + ); +*) + ignore (self#buffer#connect#insert_text + ~callback: + (fun it s -> + if !undo_lock && not (Queue.is_empty redo) then begin + Stack.iter (fun e -> Stack.push (neg e) history) nredo; + Stack.clear nredo; + 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; + let start_offset = start#offset in + let stop_offset = stop#offset in + let s = self#buffer#get_text ~start ~stop () in +(* if Stack.is_empty history or (match Stack.top history with + | Delete(old,opos,olen) -> + olen=1 or opos <> start_offset + | _ -> true + ) + then +*) Stack.push + (Delete(s, + start_offset, + stop_offset - start_offset + )) + history + (* else begin + match Stack.pop history with + | Delete(olds,offset,len) -> + Stack.push + (Delete(olds^s, + offset, + len+(Glib.Utf8.length s))) + history + | _ -> assert false + + end*); + self#dump_debug + )) +end + +let undoable_view ?(buffer:GText.buffer option) = + GtkText.View.make_params [] + ~cont:(GContainer.pack_container + ~create: + (fun pl -> let w = match buffer with + | None -> GtkText.View.create [] + | Some b -> GtkText.View.create_with_buffer b#as_buffer + in + Gobject.set_params w pl; ((new undoable_view w):undoable_view))) + + |