1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: undo.ml 7603 2005-11-23 17:21:53Z barras $ *)
14
| Insert of string * int * int (* content*pos*length *)
15
| Delete of string * int * int (* content*pos*length *)
17
let neg act = match act with
18
| Insert (s,i,l) -> Delete (s,i,l)
19
| Delete (s,i,l) -> Insert (s,i,l)
21
class undoable_view (tv:[>Gtk.text_view] Gtk.obj) =
22
let undo_lock = ref true in
24
inherit GText.view tv as super
25
val history = (Stack.create () : action Stack.t)
26
val redo = (Queue.create () : action Queue.t)
27
val nredo = (Stack.create () : action Stack.t)
29
method private dump_debug =
30
if false (* !debug *) then begin
31
prerr_endline "==========Stack top=============";
33
(fun e -> match e with
35
Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
37
Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
39
Printf.eprintf "Stack size %d\n" (Stack.length history);
40
prerr_endline "==========Stack Bottom==========";
41
prerr_endline "==========Queue start=============";
43
(fun e -> match e with
45
Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
47
Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l)
49
Printf.eprintf "Stack size %d\n" (Queue.length redo);
50
prerr_endline "==========Queue End=========="
54
method clear_undo = Stack.clear history; Stack.clear nredo; Queue.clear redo
56
method undo = if !undo_lock then begin
61
match Stack.pop history with
62
| Insert(s,p,l) as act ->
63
let start = self#buffer#get_iter_at_char p in
64
(self#buffer#delete_interactive
66
~stop:(start#forward_chars l)
68
(Stack.push act history; false)
69
| Delete(s,p,l) as act ->
70
let iter = self#buffer#get_iter_at_char p in
71
(self#buffer#insert_interactive ~iter s) or
72
(Stack.push act history; false)
74
let act = Stack.pop history in
85
(prerr_endline "UNDO DISCARDED"; true)
87
method redo = prerr_endline "REDO"; true
89
(* INCORRECT: is called even while undoing...
90
ignore (self#buffer#connect#mark_set
92
(fun it tm -> if !undo_lock && not (Queue.is_empty redo) then begin
93
Stack.iter (fun e -> Stack.push (neg e) history) nredo;
95
Queue.iter (fun e -> Stack.push e history) redo;
100
ignore (self#buffer#connect#insert_text
103
if !undo_lock && not (Queue.is_empty redo) then begin
104
Stack.iter (fun e -> Stack.push (neg e) history) nredo;
106
Queue.iter (fun e -> Stack.push e history) redo;
109
(* let pos = it#offset in
110
if Stack.is_empty history or
111
s=" " or s="\t" or s="\n" or
112
(match Stack.top history with
113
| Insert(old,opos,olen) ->
117
Stack.push (Insert(s,it#offset,Glib.Utf8.length s)) history
119
match Stack.pop history with
120
| Insert(olds,offset,len) ->
124
len+(Glib.Utf8.length s)))
130
ignore (self#buffer#connect#delete_range
133
if !undo_lock && not (Queue.is_empty redo) then begin
134
Queue.iter (fun e -> Stack.push e history) redo;
137
let start_offset = start#offset in
138
let stop_offset = stop#offset in
139
let s = self#buffer#get_text ~start ~stop () in
140
(* if Stack.is_empty history or (match Stack.top history with
141
| Delete(old,opos,olen) ->
142
olen=1 or opos <> start_offset
149
stop_offset - start_offset
153
match Stack.pop history with
154
| Delete(olds,offset,len) ->
158
len+(Glib.Utf8.length s)))
167
let undoable_view ?(buffer:GText.buffer option) =
168
GtkText.View.make_params []
169
~cont:(GContainer.pack_container
171
(fun pl -> let w = match buffer with
172
| None -> GtkText.View.create []
173
| Some b -> GtkText.View.create_with_buffer b#as_buffer
175
Gobject.set_params w pl; ((new undoable_view w):undoable_view)))