aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/document.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-21 00:14:13 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-21 00:14:13 +0100
commitc5d0aa889fa80404f6c291000938e443d6200e5b (patch)
tree253fbb6ebe405b78b5e66a1e1f7d4da606dbfa78 /ide/document.ml
parenta4b457bef4290fed3f2869795f1539de53b3805a (diff)
parente54d014ce10dea4a74b66e5091d25e4b26bd71fa (diff)
Merge branch 'v8.5'
Diffstat (limited to 'ide/document.ml')
-rw-r--r--ide/document.ml27
1 files changed, 17 insertions, 10 deletions
diff --git a/ide/document.ml b/ide/document.ml
index bb431e791..62457fe56 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -16,8 +16,8 @@ type id = Stateid.t
class type ['a] signals =
object
- method popped : callback:('a -> unit) -> unit
- method pushed : callback:('a -> unit) -> unit
+ method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+ method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
end
class ['a] signal () =
@@ -32,14 +32,14 @@ end
type 'a document = {
mutable stack : 'a sentence list;
mutable context : ('a sentence list * 'a sentence list) option;
- pushed_sig : 'a signal;
- popped_sig : 'a signal;
+ pushed_sig : ('a * ('a list * 'a list) option) signal;
+ popped_sig : ('a * ('a list * 'a list) option) signal;
}
-let connect d =
+let connect d : 'a signals =
object
- method pushed ~callback = d.pushed_sig#connect callback
- method popped ~callback = d.popped_sig#connect callback
+ method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx)
+ method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx)
end
let create () = {
@@ -49,6 +49,12 @@ let create () = {
popped_sig = new signal ();
}
+let repr_context s = match s.context with
+| None -> None
+| Some (cl, cr) ->
+ let map s = s.data in
+ Some (List.map map cl, List.map map cr)
+
(* Invariant, only the tip is a allowed to have state_id = None *)
let invariant l = l = [] || (List.hd l).state_id <> None
@@ -64,12 +70,13 @@ let tip_data = function
let push d x =
assert(invariant d.stack);
d.stack <- { data = x; state_id = None } :: d.stack;
- d.pushed_sig#call x
+ d.pushed_sig#call (x, repr_context d)
let pop = function
| { stack = [] } -> raise Empty
- | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data
-
+ | { stack = { data }::xs } as s ->
+ s.stack <- xs; s.popped_sig#call (data, repr_context s); data
+
let focus d ~cond_top:c_start ~cond_bot:c_stop =
assert(invariant d.stack);
if d.context <> None then invalid_arg "focus";