Source file `b_update.ml`

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
(* This is where we store the widgets that receive the update event *)

(* similar to Sync.ml but we make sure there is no repeated entries in the
   queue *)

(* see: examples/chain *)

(* TODO à vider en sortant ? *)
(* ou à attacher à la board ? *)

open B_utils
module Trigger =  B_trigger
module Var = B_var
module Widget = B_widget

let str = Printf.sprintf

let table : (Widget.t list) Var.t = Var.create  []

let is_empty () =
  Var.get table = []

let clear () =
  if not (is_empty ()) then
    begin
      printd debug_warning "The update queue was not empty";
      Var.set table []
    end

let mem w =
  List.exists (Widget.equal w) (Var.get table)

let push w =
  if mem w then
    printd debug_event "Widget #%u is already in the Update.table" w.Widget.wid
  else begin
    Var.update table (List.cons w);
    Trigger.push_update w.Widget.wid;
  end

let push_all () =
  List.iter
    (fun w -> Trigger.push_update (Widget.id w)) (Var.get table)

let execute_one e w =
  if w.Widget.wid = Trigger.get_update_wid e
  then (
    Widget.wake_up_all e w;
    Trigger.push_redraw (Widget.id w) (* OK?? *)
  )

let execute e =
  match Var.get table with
  | [] -> () (* Optimization (?) we don't want to reset the table to
                [] if it was already empty *)
  | list -> (
      Var.protect table;
      let wid = Trigger.get_update_wid e in
      let list_e, other = List.partition (fun w -> w.Widget.wid = wid) list in
      printd debug_memory "Udpate Table: remaining size=%i" (List.length other);
      (* we keep the widgets that do not correspond to the event e *)
      Var.unsafe_set table other;
      Var.release table;
      (* we release the table before execution so that one can still push to
         the new table while the old one is being executed *)
      printd debug_memory "Update Table: execute size=%i" (List.length list_e);
      List.iter (execute_one e) list_e)