more explicit type Exec.context;
authorwenzelm
Thu Jul 11 23:24:40 2013 +0200 (2013-07-11)
changeset 52604ff2f0818aebc
parent 52603 a44e9a1d5d8b
child 52605 a2a805549c74
more explicit type Exec.context;
eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/exec.ML
src/Pure/PIDE/protocol.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 22:53:56 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 23:24:40 2013 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    type exec = eval * print list
     1.5    val no_exec: exec
     1.6    val exec_ids: exec option -> Document_ID.exec list
     1.7 -  val exec: exec -> unit
     1.8 +  val exec: Exec.context -> exec -> unit
     1.9  end;
    1.10  
    1.11  structure Command: COMMAND =
    1.12 @@ -43,32 +43,31 @@
    1.13      Result res => Exn.release res
    1.14    | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    1.15  
    1.16 -fun memo_exec (Memo v) =
    1.17 +fun memo_exec context (Memo v) =
    1.18    (case Synchronized.value v of
    1.19      Result res => res
    1.20 -  | Expr (exec_id, _) =>
    1.21 +  | Expr _ =>
    1.22        Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
    1.23          (fn Result res => SOME (res, Result res)
    1.24 -          | Expr (exec_id, e) =>
    1.25 +          | expr as Expr (exec_id, e) =>
    1.26                uninterruptible (fn restore_attributes => fn () =>
    1.27 -                let
    1.28 -                  val _ = Exec.running exec_id;
    1.29 -                  val res = Exn.capture (restore_attributes e) ();
    1.30 -                  val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.31 -                in SOME (res, Result res) end) ())
    1.32 -      |> (fn NONE => error ("Concurrent execution attempt: " ^ Document_ID.print exec_id)
    1.33 -           | SOME res => res))
    1.34 -  |> Exn.release;
    1.35 +                if Exec.running context exec_id then
    1.36 +                  let
    1.37 +                    val res = Exn.capture (restore_attributes e) ();
    1.38 +                    val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.39 +                  in SOME (res, Result res) end
    1.40 +                else SOME (Exn.interrupt_exn, expr)) ())
    1.41 +      |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.42 +  |> Exn.release |> ignore;
    1.43  
    1.44 -fun memo_fork params (Memo v) =
    1.45 +fun memo_fork params context (Memo v) =
    1.46    (case Synchronized.value v of
    1.47      Result _ => ()
    1.48 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec (Memo v))));
    1.49 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec context (Memo v))));
    1.50  
    1.51  end;
    1.52  
    1.53  
    1.54 -
    1.55  (** main phases of execution **)
    1.56  
    1.57  (* read *)
    1.58 @@ -277,15 +276,15 @@
    1.59  
    1.60  local
    1.61  
    1.62 -fun run_print (Print {name, pri, print_process, ...}) =
    1.63 +fun run_print context (Print {name, pri, print_process, ...}) =
    1.64    (if Multithreading.enabled () then
    1.65      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
    1.66 -  else memo_exec) print_process;
    1.67 +  else memo_exec) context print_process;
    1.68  
    1.69  in
    1.70  
    1.71 -fun exec (Eval {eval_process, ...}, prints) =
    1.72 -  (memo_exec eval_process; List.app run_print prints);
    1.73 +fun exec context (Eval {eval_process, ...}, prints) =
    1.74 +  (memo_exec context eval_process; List.app (run_print context) prints);
    1.75  
    1.76  end;
    1.77  
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 22:53:56 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 23:24:40 2013 +0200
     2.3 @@ -202,27 +202,14 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* associated execution *)
     2.8 -
     2.9 -type execution =
    2.10 - {version_id: Document_ID.version,
    2.11 -  group: Future.group,
    2.12 -  continue: bool Synchronized.var};
    2.13 -
    2.14 -val no_execution =
    2.15 - {version_id = Document_ID.none,
    2.16 -  group = Future.new_group NONE,
    2.17 -  continue = Synchronized.var "continue" false};
    2.18 -
    2.19 -fun make_execution version_id =
    2.20 - {version_id = version_id,
    2.21 -  group = Future.new_group NONE,
    2.22 -  continue = Synchronized.var "continue" true};
    2.23 -
    2.24 -
    2.25  
    2.26  (** main state -- document structure and execution process **)
    2.27  
    2.28 +type execution = {version_id: Document_ID.version, context: Exec.context};
    2.29 +
    2.30 +val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
    2.31 +fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
    2.32 +
    2.33  abstype state = State of
    2.34   {versions: version Inttab.table,  (*version id -> document content*)
    2.35    commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
    2.36 @@ -307,34 +294,35 @@
    2.37    in (versions', commands', execution) end);
    2.38  
    2.39  
    2.40 -
    2.41 -(** document execution **)
    2.42 +(* document execution *)
    2.43  
    2.44 -val discontinue_execution =
    2.45 -  execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
    2.46 +fun discontinue_execution state =
    2.47 +  Exec.drop_context (#context (execution_of state));
    2.48  
    2.49 -val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
    2.50 +fun cancel_execution state =
    2.51 +  (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
    2.52  
    2.53  fun start_execution state =
    2.54    let
    2.55 -    val {version_id, group, continue} = execution_of state;
    2.56 -    fun running () = Synchronized.guarded_access continue (fn x => SOME (x, x));
    2.57 +    val {version_id, context} = execution_of state;
    2.58      val _ =
    2.59 -      if not (running ()) orelse Task_Queue.is_canceled group then []
    2.60 -      else
    2.61 +      if Exec.is_running context then
    2.62          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.63            (fn deps => fn (name, node) =>
    2.64              if not (visible_node node) andalso finished_theory node then
    2.65                Future.value ()
    2.66              else
    2.67                (singleton o Future.forks)
    2.68 -                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    2.69 +                {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.70                    deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    2.71                  (fn () =>
    2.72                    iterate_entries (fn (_, opt_exec) => fn () =>
    2.73                      (case opt_exec of
    2.74 -                      SOME exec => if running () then SOME (Command.exec exec) else NONE
    2.75 -                    | NONE => NONE)) node ()));
    2.76 +                      SOME exec =>
    2.77 +                        if Exec.is_running context then SOME (Command.exec context exec)
    2.78 +                        else NONE
    2.79 +                    | NONE => NONE)) node ()))
    2.80 +      else [];
    2.81    in () end;
    2.82  
    2.83  
     3.1 --- a/src/Pure/PIDE/exec.ML	Thu Jul 11 22:53:56 2013 +0200
     3.2 +++ b/src/Pure/PIDE/exec.ML	Thu Jul 11 23:24:40 2013 +0200
     3.3 @@ -6,49 +6,95 @@
     3.4  
     3.5  signature EXEC =
     3.6  sig
     3.7 -  val running: Document_ID.exec -> unit
     3.8 +  type context
     3.9 +  val no_context: context
    3.10 +  val drop_context: context -> unit
    3.11 +  val fresh_context: unit -> context
    3.12 +  val is_running: context -> bool
    3.13 +  val running: context -> Document_ID.exec -> bool
    3.14    val finished: Document_ID.exec -> bool -> unit
    3.15    val is_stable: Document_ID.exec -> bool
    3.16    val peek_running: Document_ID.exec -> Future.group option
    3.17 -  val purge_unstable: unit -> unit
    3.18 +  val purge_canceled: unit -> unit
    3.19 +  val terminate_all: unit -> unit
    3.20  end;
    3.21  
    3.22  structure Exec: EXEC =
    3.23  struct
    3.24  
    3.25 -type status = Future.group option;  (*SOME group: running, NONE: canceled/unstable*)
    3.26 -val execs = Synchronized.var "Exec.execs" (Inttab.empty: status Inttab.table);
    3.27 +(* global state *)
    3.28 +
    3.29 +datatype context = Context of Document_ID.generic;
    3.30 +val no_context = Context Document_ID.none;
    3.31 +
    3.32 +type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    3.33 +val state = Synchronized.var "Exec.state" (no_context, Inttab.empty: status Inttab.table);
    3.34  
    3.35 -fun running exec_id =
    3.36 +
    3.37 +(* unique execution context *)
    3.38 +
    3.39 +fun drop_context context =
    3.40 +  Synchronized.change state
    3.41 +    (apfst (fn context' => if context = context' then no_context else context'));
    3.42 +
    3.43 +fun fresh_context () =
    3.44    let
    3.45 -    val group =
    3.46 -      (case Future.worker_group () of
    3.47 -        SOME group => group
    3.48 -      | NONE => error ("Missing worker thread context for execution " ^ Document_ID.print exec_id));
    3.49 -  in Synchronized.change execs (Inttab.update_new (exec_id, SOME group)) end;
    3.50 +    val context = Context (Document_ID.make ());
    3.51 +    val _ = Synchronized.change state (apfst (K context));
    3.52 +  in context end;
    3.53 +
    3.54 +fun is_running context = context = fst (Synchronized.value state);
    3.55 +
    3.56 +
    3.57 +(* registered execs *)
    3.58 +
    3.59 +fun running context exec_id =
    3.60 +  Synchronized.guarded_access state
    3.61 +    (fn (current_context, execs) =>
    3.62 +      let
    3.63 +        val cont = context = current_context;
    3.64 +        val execs' =
    3.65 +          if cont then
    3.66 +            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    3.67 +              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    3.68 +          else execs;
    3.69 +      in SOME (cont, (current_context, execs')) end);
    3.70  
    3.71  fun finished exec_id stable =
    3.72 -  Synchronized.change execs
    3.73 -    (if stable then Inttab.delete exec_id else Inttab.update (exec_id, NONE));
    3.74 +  Synchronized.change state
    3.75 +    (apsnd (fn execs =>
    3.76 +      if not (Inttab.defined execs exec_id) then
    3.77 +        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    3.78 +      else if stable then Inttab.delete exec_id execs
    3.79 +      else Inttab.update (exec_id, NONE) execs));
    3.80  
    3.81  fun is_stable exec_id =
    3.82    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    3.83 -  (case Inttab.lookup (Synchronized.value execs) exec_id of
    3.84 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.85      NONE => true
    3.86    | SOME status => is_some status);
    3.87  
    3.88  fun peek_running exec_id =
    3.89 -  (case Inttab.lookup (Synchronized.value execs) exec_id of
    3.90 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.91      SOME (SOME group) => SOME group
    3.92    | _ => NONE);
    3.93  
    3.94 -fun purge_unstable () =
    3.95 -  Synchronized.guarded_access execs
    3.96 -    (fn tab =>
    3.97 +fun purge_canceled () =
    3.98 +  Synchronized.guarded_access state
    3.99 +    (fn (context, execs) =>
   3.100        let
   3.101 -        val unstable = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) tab [];
   3.102 -        val tab' = fold Inttab.delete unstable tab;
   3.103 -      in SOME ((), tab') end);
   3.104 +        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
   3.105 +        val execs' = fold Inttab.delete canceled execs;
   3.106 +      in SOME ((), (context, execs')) end);
   3.107 +
   3.108 +fun terminate_all () =
   3.109 +  let
   3.110 +    val groups =
   3.111 +      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
   3.112 +        (snd (Synchronized.value state)) [];
   3.113 +    val _ = List.app Future.cancel_group groups;
   3.114 +    val _ = List.app Future.terminate groups;
   3.115 +  in () end;
   3.116  
   3.117  end;
   3.118  
     4.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jul 11 22:53:56 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Jul 11 23:24:40 2013 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4          val (assign_update, state') = Document.update old_id new_id edits state;
     4.5  
     4.6          val _ = List.app Future.cancel_group (Goal.reset_futures ());
     4.7 -        val _ = Exec.purge_unstable ();
     4.8 +        val _ = Exec.purge_canceled ();
     4.9          val _ = Isabelle_Process.reset_tracing ();
    4.10  
    4.11          val _ =