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 +(* document execution *)
2.41
2.42 -(** document execution **)
2.43 +fun discontinue_execution state =
2.44 + Exec.drop_context (#context (execution_of state));
2.45
2.46 -val discontinue_execution =
2.47 - execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
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 -fun running exec_id =
3.30 +datatype context = Context of Document_ID.generic;
3.31 +val no_context = Context Document_ID.none;
3.32 +
3.33 +type status = Future.group option; (*SOME group: running, NONE: canceled*)
3.34 +val state = Synchronized.var "Exec.state" (no_context, Inttab.empty: status Inttab.table);
3.35 +
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 _ =