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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(************************************************************************)
(* 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$ *)
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
Some(d,Bstack.top bs,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 = 1 & n > 0 then
errorlabstrm "Edit.undo" (str"Undo stack exhausted");
repeat n Bstack.pop bs
(* Return the depth of the focused proof of [e] stack, this is used to
put informations in coq prompt (in emacs mode). *)
let depth e =
match e.focus with
| None -> invalid_arg "Edit.depth"
| Some d ->
let (bs,_) = Hashtbl.find e.buf d in
Bstack.depth bs
(* Undo focused proof of [e] to reach depth [n] *)
let undo_todepth e n =
match e.focus with
| None ->
if n <> 0
then errorlabstrm "Edit.undo_todepth" (str"No proof in progress")
else () (* if there is no proof in progress, then n must be zero *)
| Some d ->
let (bs,_) = Hashtbl.find e.buf d in
if Bstack.depth bs < n then
errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
repeat (Bstack.depth bs - n) Bstack.pop bs
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 b in
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
|
