tuned -- more explicit types;
authorwenzelm
Sat Jun 02 21:10:20 2018 +0200 (14 months ago)
changeset 6835329cbe9e8ecde
parent 68352 38272f9481c2
child 68354 93d3c967802e
tuned -- more explicit types;
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/execution.ML	Sat Jun 02 19:52:16 2018 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Sat Jun 02 21:10:20 2018 +0200
     1.3 @@ -31,17 +31,34 @@
     1.4  (* global state *)
     1.5  
     1.6  type print = {name: string, pri: int, body: unit -> unit};
     1.7 -type exec_state = Future.group list * print list;  (*active forks, prints*)
     1.8 -type state =
     1.9 -  Document_ID.execution * (*overall document execution*)
    1.10 -  exec_state Inttab.table;  (*running command execs*)
    1.11 +type execs = (Future.group list * print list) (*active forks, prints*) Inttab.table;
    1.12 +val init_execs: execs = Inttab.make [(Document_ID.none, ([], []))];
    1.13 +
    1.14 +datatype state =
    1.15 +  State of
    1.16 +   {execution_id: Document_ID.execution,  (*overall document execution*)
    1.17 +    execs: execs};  (*running command execs*)
    1.18 +
    1.19 +fun make_state (execution_id, execs) =
    1.20 +  State {execution_id = execution_id, execs = execs};
    1.21  
    1.22 -val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
    1.23 -val state = Synchronized.var "Execution.state" init_state;
    1.24 +local
    1.25 +  val state =
    1.26 +    Synchronized.var "Execution.state" (make_state (Document_ID.none, init_execs));
    1.27 +in
    1.28 +
    1.29 +fun get_state () = let val State args = Synchronized.value state in args end;
    1.30  
    1.31 -fun get_state () = Synchronized.value state;
    1.32 -fun change_state_result f = Synchronized.change_result state f;
    1.33 -fun change_state f = Synchronized.change state f;
    1.34 +fun change_state_result f =
    1.35 +  Synchronized.change_result state (fn (State {execution_id, execs}) =>
    1.36 +    let val (result, args') = f (execution_id, execs)
    1.37 +    in (result, make_state args') end);
    1.38 +
    1.39 +fun change_state f =
    1.40 +  Synchronized.change state (fn (State {execution_id, execs}) =>
    1.41 +    make_state (f (execution_id, execs)));
    1.42 +
    1.43 +end;
    1.44  
    1.45  fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
    1.46  
    1.47 @@ -56,13 +73,14 @@
    1.48  
    1.49  fun discontinue () = change_state (apfst (K Document_ID.none));
    1.50  
    1.51 -fun is_running execution_id = execution_id = #1 (get_state ());
    1.52 +fun is_running execution_id =
    1.53 +  execution_id = #execution_id (get_state ());
    1.54  
    1.55  
    1.56  (* running execs *)
    1.57  
    1.58  fun is_running_exec exec_id =
    1.59 -  Inttab.defined (#2 (get_state ())) exec_id;
    1.60 +  Inttab.defined (#execs (get_state ())) exec_id;
    1.61  
    1.62  fun running execution_id exec_id groups =
    1.63    change_state_result (fn (execution_id', execs) =>
    1.64 @@ -74,13 +92,13 @@
    1.65  
    1.66  (* exec groups and tasks *)
    1.67  
    1.68 -fun exec_groups ((_, execs): state) exec_id =
    1.69 +fun exec_groups (execs: execs) exec_id =
    1.70    (case Inttab.lookup execs exec_id of
    1.71      SOME (groups, _) => groups
    1.72    | NONE => []);
    1.73  
    1.74  fun snapshot exec_ids =
    1.75 -  change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids)));
    1.76 +  change_state_result (`(fn (_, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
    1.77  
    1.78  fun join exec_ids =
    1.79    (case snapshot exec_ids of
    1.80 @@ -91,7 +109,7 @@
    1.81            deps = tasks, pri = 0, interrupts = false} I
    1.82        |> Future.join; join exec_ids));
    1.83  
    1.84 -fun peek exec_id = exec_groups (get_state ()) exec_id;
    1.85 +fun peek exec_id = exec_groups (#execs (get_state ())) exec_id;
    1.86  
    1.87  fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
    1.88  
    1.89 @@ -160,7 +178,7 @@
    1.90      end));
    1.91  
    1.92  fun fork_prints exec_id =
    1.93 -  (case Inttab.lookup (#2 (get_state ())) exec_id of
    1.94 +  (case Inttab.lookup (#execs (get_state ())) exec_id of
    1.95      SOME (_, prints) =>
    1.96        if Future.relevant prints then
    1.97          let val pos = Position.thread_data () in
    1.98 @@ -188,7 +206,7 @@
    1.99  fun reset () =
   1.100    change_state_result (fn (_, execs) =>
   1.101      let val groups = Inttab.fold (append o #1 o #2) execs []
   1.102 -    in (groups, init_state) end);
   1.103 +    in (groups, (Document_ID.none, init_execs)) end);
   1.104  
   1.105  fun shutdown () =
   1.106    (Future.shutdown ();
   1.107 @@ -197,4 +215,3 @@
   1.108      | exns => raise Par_Exn.make exns));
   1.109  
   1.110  end;
   1.111 -