From 1da3072af8182940641bf42316ffaa01cade77b3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 5 Jan 2015 11:50:21 +0100 Subject: Removing GUtil dependency from ide/document.ml. We reimplement a quick-n-dirty Gtk-free signal handler. --- ide/document.ml | 34 ++++++++++++++++++++++------------ 1 file changed, 22 insertions(+), 12 deletions(-) (limited to 'ide/document.ml') diff --git a/ide/document.ml b/ide/document.ml index 34fcce1b6..9823e7576 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -14,29 +14,39 @@ type 'a sentence = { mutable state_id : Stateid.t option; data : 'a } type id = Stateid.t -class ['a] signals - (pushed : 'a GUtil.signal) - (popped : 'a GUtil.signal) = -object (self) - inherit GUtil.ml_signals [pushed#disconnect; popped#disconnect] - method pushed = pushed#connect ~after - method popped = popped#connect ~after +class type ['a] signals = + object + method popped : callback:('a -> unit) -> unit + method pushed : callback:('a -> unit) -> unit + end + +class ['a] signal () = +object + val mutable attached : ('a -> unit) list = [] + method call (x : 'a) = + let iter f = try f x with _ -> () in + List.iter iter attached + method connect f = attached <- f :: attached end type 'a document = { mutable stack : 'a sentence list; mutable context : ('a sentence list * 'a sentence list) option; - pushed_sig : 'a GUtil.signal; - popped_sig : 'a GUtil.signal; + pushed_sig : 'a signal; + popped_sig : 'a signal; } -let connect d = new signals d.pushed_sig d.popped_sig +let connect d = + object + method pushed ~callback = d.pushed_sig#connect callback + method popped ~callback = d.popped_sig#connect callback + end let create () = { stack = []; context = None; - pushed_sig = new GUtil.signal (); - popped_sig = new GUtil.signal (); + pushed_sig = new signal (); + popped_sig = new signal (); } (* Invariant, only the tip is a allowed to have state_id = None *) -- cgit v1.2.3