1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
type ('a,'b,'c) t = {
mutable focus : 'a option;
mutable last_focused_stk : 'a list;
buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
let empty () = {
focus = None;
last_focused_stk = [];
buf = Hashtbl.create 17 }
let focus e nd =
if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
begin match e.focus with
| Some foc when foc <> nd ->
e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
| _ -> ()
end;
e.focus <- Some nd
let unfocus e =
match e.focus with
| None -> invalid_arg "Edit.unfocus"
| Some foc ->
begin
e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
e.focus <- None
end
let last_focused e =
match e.last_focused_stk with
| [] -> None
| f::_ -> Some f
let restore_last_focus e =
match e.last_focused_stk with
| [] -> ()
| f::_ -> focus e f
let focusedp e =
match e.focus with
| None -> false
| _ -> true
let read e =
match e.focus with
| None -> None
| Some d ->
let (bs,c) = Hashtbl.find e.buf d in
(match Bstack.top bs with
| None -> anomaly "Edit.read"
| Some v -> Some(d,v,c))
let mutate e f =
match e.focus with
| None -> invalid_arg "Edit.mutate"
| Some d ->
let (bs,c) = Hashtbl.find e.buf d in
Bstack.app_push bs (f c)
let rev_mutate e f =
match e.focus with
| None -> invalid_arg "Edit.rev_mutate"
| Some d ->
let (bs,c) = Hashtbl.find e.buf d in
Bstack.app_repl bs (f c)
let undo e n =
match e.focus with
| None -> invalid_arg "Edit.undo"
| Some d ->
let (bs,_) = Hashtbl.find e.buf d in
if Bstack.depth bs <= n then
errorlabstrm "Edit.undo" (str"Undo stack would be exhausted");
repeat n (fun () -> let _ = Bstack.pop bs in ()) ()
let create e (d,b,c,udepth) =
if Hashtbl.mem e.buf d then
errorlabstrm "Edit.create"
(str"Already editing something of that name");
let bs = Bstack.create udepth in
Bstack.push bs b;
Hashtbl.add e.buf d (bs,c)
let delete e d =
if not(Hashtbl.mem e.buf d) then
errorlabstrm "Edit.delete" (str"No such editor");
Hashtbl.remove e.buf d;
e.last_focused_stk <- (list_except d e.last_focused_stk);
match e.focus with
| Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
| None -> ()
let dom e =
let l = ref [] in
Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
!l
let clear e =
e.focus <- None;
e.last_focused_stk <- [];
Hashtbl.clear e.buf
|
