blob: fb96cb6d7644cc6a947463ae0d56174799ccb69f (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* An 'a document is a structure to hold and manipulate list of sentences.
Sentences are equipped with an id = Stateid.t and can carry arbitrary
data ('a).
When added (push) to the document, a sentence has no id, it has
be manually assigned just afterward or the sentence has to be removed
(pop) before any other sentence can be pushed.
This exception is useful since the process of assigning an id to
a sentence may fail (parse error) and an error handler may want to annotate
a script buffer with the error message. This handler needs to find the
sentence in question, and it is simpler if the sentence is in the document.
Only the functions pop, find, fold_all and find_map can be called on a
document with a tip that has no id (and assign_tip_id of course).
The document can be focused (non recursively) to a zone. After that
some functions operate on the focused zone only. When unfocused the
context (the part of the document out of focus) is restored.
*)
exception Empty
type 'a document
type id = Stateid.t
val create : unit -> 'a document
(* Functions that work on the focused part of the document ******************* *)
(** The last sentence. @raise Invalid_argument if tip has no id. @raise Empty *)
val tip : 'a document -> id
(** The last sentence. @raise Empty *)
val tip_data : 'a document -> 'a
(** Add a sentence on the top (with no state_id) *)
val push : 'a document -> 'a -> unit
(** Remove the tip setence. @raise Empty *)
val pop : 'a document -> 'a
(** Assign the state_id of the tip. @raise Empty *)
val assign_tip_id : 'a document -> id -> unit
(** [cut_at d id] cuts the document at [id] that is the new tip.
Returns the list of sentences that were cut.
@raise Not_found *)
val cut_at : 'a document -> id -> 'a list
(* Functions that work on the whole document ********************************* *)
(** returns the id of the topmost sentence validating the predicate and
a boolean that is true if one needs to unfocus the document to access
such sentence. @raise Not_found *)
val find_id : 'a document -> (id -> 'a -> bool) -> id * bool
(** look for a sentence validating the predicate. The boolean is true
if the sentence is in the zone currently focused. @raise Not_found *)
val find : 'a document -> (bool -> id option -> 'a -> bool) -> 'a
val find_map : 'a document -> (bool -> id option -> 'a -> 'b option) -> 'b
(** After [focus s c1 c2] the top of [s] is the topmost element [x] such that
[c1 x] is [true] and the bottom is the first element [y] following [x]
such that [c2 y] is [true].
@raise Invalid_argument if there is no such [x] and [y] or already focused *)
val focus :
'a document ->
cond_top:(id -> 'a -> bool) -> cond_bot:(id -> 'a -> bool) -> unit
(** Undoes a [focus].
@raise Invalid_argument "CStack.unfocus" if the stack is not focused *)
val unfocus : 'a document -> unit
(** Is the document focused *)
val focused : 'a document -> bool
(** No sentences at all *)
val is_empty : 'a document -> bool
(** returns the 1 to-last sentence, and true if we need to unfocus to reach it.
@raise Not_found *)
val before_tip : 'a document -> id * bool
(** Is the id in the focused zone? *)
val is_in_focus : 'a document -> id -> bool
(** Folds over the whole document starting from the topmost (maybe unfocused)
sentence. *)
val fold_all :
'a document -> 'c -> ('c -> bool -> id option -> 'a -> 'c) -> 'c
(** Returns (top,bot) such that the document is morally (top @ s @ bot) where
s is the focused part. @raise Invalid_argument *)
val context : 'a document -> (id * 'a) list * (id * 'a) list
(** debug print *)
val print :
'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds
(** Callbacks on documents *)
class type ['a] signals =
object
method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
end
val connect : 'a document -> 'a signals
|
