diff options
Diffstat (limited to 'ide/undo.ml')
| -rw-r--r-- | ide/undo.ml | 175 |
1 files changed, 0 insertions, 175 deletions
diff --git a/ide/undo.ml b/ide/undo.ml deleted file mode 100644 index 8456cf9f..00000000 --- a/ide/undo.ml +++ /dev/null @@ -1,175 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Ideutils -open GText -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 - 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))) - - |