diff options
Diffstat (limited to 'ide/undo.ml')
-rw-r--r-- | ide/undo.ml | 68 |
1 files changed, 34 insertions, 34 deletions
diff --git a/ide/undo.ml b/ide/undo.ml index f617d289..18c2f7a4 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -6,20 +6,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: undo.ml 7603 2005-11-23 17:21:53Z barras $ *) +(* $Id$ *) open GText open Ideutils -type action = - | Insert of string * int * int (* content*pos*length *) - | Delete of string * int * int (* content*pos*length *) +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 + let undo_lock = ref true in object(self) inherit GText.view tv as super val history = (Stack.create () : action Stack.t) @@ -29,25 +29,25 @@ object(self) method private dump_debug = if false (* !debug *) then begin prerr_endline "==========Stack top============="; - Stack.iter + 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) -> + | 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 + 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) -> + | 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==========" + prerr_endline "==========Queue End==========" end @@ -57,16 +57,16 @@ object(self) undo_lock := false; prerr_endline "UNDO"; try begin - let r = + let r = match Stack.pop history with - | Insert(s,p,l) as act -> + | Insert(s,p,l) as act -> let start = self#buffer#get_iter_at_char p in - (self#buffer#delete_interactive + (self#buffer#delete_interactive ~start ~stop:(start#forward_chars l) ()) or (Stack.push act history; false) - | Delete(s,p,l) as act -> + | 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) @@ -75,11 +75,11 @@ object(self) Queue.push act redo; Stack.push act nredo end; - undo_lock := true; + undo_lock := true; r end - with Stack.Empty -> - undo_lock := true; + with Stack.Empty -> + undo_lock := true; false end else (prerr_endline "UNDO DISCARDED"; true) @@ -97,7 +97,7 @@ object(self) end) ); *) - ignore (self#buffer#connect#insert_text + ignore (self#buffer#connect#insert_text ~callback: (fun it s -> if !undo_lock && not (Queue.is_empty redo) then begin @@ -107,18 +107,18 @@ object(self) Queue.clear redo; end; (* let pos = it#offset in - if Stack.is_empty history or + if Stack.is_empty history or s=" " or s="\t" or s="\n" or - (match Stack.top history with - | Insert(old,opos,olen) -> + (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,offset,len) -> + Stack.push (Insert(olds^s, offset, len+(Glib.Utf8.length s))) @@ -129,7 +129,7 @@ object(self) )); ignore (self#buffer#connect#delete_range ~callback: - (fun ~start ~stop -> + (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; @@ -138,12 +138,12 @@ object(self) 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) -> + | Delete(old,opos,olen) -> olen=1 or opos <> start_offset | _ -> true ) then -*) Stack.push +*) Stack.push (Delete(s, start_offset, stop_offset - start_offset @@ -151,27 +151,27 @@ object(self) history (* else begin match Stack.pop history with - | Delete(olds,offset,len) -> - Stack.push + | 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 + GtkText.View.make_params [] + ~cont:(GContainer.pack_container ~create: - (fun pl -> let w = match buffer with + (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))) - - + + |