--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri Jul 12 13:12:21 2013 +0200
@@ -75,7 +75,7 @@
apply(unfold Mutator_def)
apply annhoare
apply(simp_all add:Redirect_Edge Color_Target)
-apply(simp add:mutator_defs Redirect_Edge_def)
+apply(simp add:mutator_defs)
done
subsection {* The Collector *}
@@ -768,7 +768,7 @@
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
@@ -789,7 +789,7 @@
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Fri Jul 12 13:12:21 2013 +0200
@@ -258,19 +258,20 @@
transformation. *}
lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-by fast
-lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)"
-by simp
-lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs)
-\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
-by simp
+ by fast
+
+lemma list_length: "length []=0" "length (x#xs) = Suc(length xs)"
+ by simp_all
+lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
+ "(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
+ by simp_all
lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-by auto
+ by auto
lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
lemmas my_simp_list = list_lemmas fst_conv snd_conv
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
Collect_mem_eq ball_simps option.simps primrecdef_list
-lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
+lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append
ML {*
fun before_interfree_simp_tac ctxt =
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Fri Jul 12 13:12:21 2013 +0200
@@ -5,7 +5,6 @@
subsection {* Proof System for Component Programs *}
declare Un_subset_iff [simp del] le_sup_iff [simp del]
-declare Cons_eq_map_conv [iff]
definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
"stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"
@@ -478,7 +477,7 @@
apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
apply (case_tac x,simp+)
apply(rule last_fst_esp,simp add:last_length)
- apply(case_tac x, (simp add:cptn_not_empty)+)
+ apply(case_tac x, simp+)
apply clarify
apply(simp add:assum_def)
apply clarify
@@ -592,7 +591,6 @@
apply simp
done
-declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
lemma Seq_sound1 [rule_format]:
"x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow>
(\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
@@ -620,7 +618,6 @@
apply(simp add:lift_def)
apply simp
done
-declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
lemma Seq_sound2 [rule_format]:
"x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x
@@ -842,7 +839,7 @@
apply(induct ys)
apply simp
apply clarify
-apply (simp add:nth_append length_append)
+apply (simp add:nth_append)
done
lemma assum_after_body:
@@ -1108,7 +1105,7 @@
apply(unfold par_cp_def)
apply (rule ccontr)
--{* By contradiction: *}
-apply (simp del: Un_subset_iff)
+apply simp
apply(erule exE)
--{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *}
apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
@@ -1128,7 +1125,7 @@
apply clarify
apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
apply (simp add:conjoin_def same_length_def)
-apply(simp add:assum_def del: Un_subset_iff)
+apply(simp add:assum_def)
apply(rule conjI)
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<in>cp (?K j) (?J j)" in allE)
apply(simp add:cp_def par_assum_def)
@@ -1136,7 +1133,7 @@
apply simp
apply clarify
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq> (?L j)" in allE)
-apply(simp del: Un_subset_iff)
+apply simp
apply(erule subsetD)
apply simp
apply(simp add:conjoin_def compat_label_def)
@@ -1206,14 +1203,14 @@
x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x;
x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
\<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
-apply(simp add: ParallelCom_def del: Un_subset_iff)
+apply(simp add: ParallelCom_def)
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prefer 2
apply simp
apply(frule rev_subsetD)
apply(erule one [THEN equalityD1])
apply(erule subsetD)
-apply (simp del: Un_subset_iff)
+apply simp
apply clarify
apply(drule_tac pre=pre and rely=rely and x=x and s=s and xs=xs and clist=clist in two)
apply(assumption+)
@@ -1256,14 +1253,14 @@
\<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely);
All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
-apply(simp add: ParallelCom_def del: Un_subset_iff)
+apply(simp add: ParallelCom_def)
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prefer 2
apply simp
apply(frule rev_subsetD)
apply(erule one [THEN equalityD1])
apply(erule subsetD)
-apply(simp del: Un_subset_iff)
+apply simp
apply clarify
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
--- a/src/Pure/Concurrent/future.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Fri Jul 12 13:12:21 2013 +0200
@@ -46,6 +46,7 @@
val new_group: group option -> group
val worker_task: unit -> task option
val worker_group: unit -> group option
+ val the_worker_group: unit -> group
val worker_subgroup: unit -> group
val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
@@ -99,6 +100,12 @@
end;
val worker_group = Option.map Task_Queue.group_of_task o worker_task;
+
+fun the_worker_group () =
+ (case worker_group () of
+ SOME group => group
+ | NONE => raise Fail "Missing worker thread context");
+
fun worker_subgroup () = new_group (worker_group ());
fun worker_guest name group f x =
@@ -556,7 +563,7 @@
val _ =
if forall is_finished xs then ()
else if Multithreading.self_critical () then
- error "Cannot join future values within critical section"
+ raise Fail "Cannot join future values within critical section"
else if is_some (worker_task ()) then join_work (map task_of xs)
else List.app (ignore o Single_Assignment.await o result_of) xs;
in map get_result xs end;
--- a/src/Pure/PIDE/command.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 12 13:12:21 2013 +0200
@@ -6,27 +6,22 @@
signature COMMAND =
sig
- type eval_process
- type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
+ val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+ type eval
+ val eval_eq: eval * eval -> bool
val eval_result_state: eval -> Toplevel.state
- type print_process
- type print =
- {name: string, pri: int, persistent: bool,
- exec_id: Document_ID.exec, print_process: print_process}
- type exec = eval * print list
- val no_exec: exec
- val exec_ids: exec option -> Document_ID.exec list
- val stable_eval: eval -> bool
- val stable_print: print -> bool
- val same_eval: eval * eval -> bool
- val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+ val eval_stable: eval -> bool
val eval: (unit -> theory) -> Token.T list -> eval -> eval
+ type print
val print: bool -> string -> eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
val print_function: {name: string, pri: int, persistent: bool} ->
({command_name: string} -> print_fn option) -> unit
val no_print_function: string -> unit
- val execute: exec -> unit
+ type exec = eval * print list
+ val no_exec: exec
+ val exec_ids: exec option -> Document_ID.exec list
+ val exec: Document_ID.execution -> exec -> unit
end;
structure Command: COMMAND =
@@ -35,40 +30,44 @@
(** memo results -- including physical interrupts! **)
datatype 'a expr =
- Expr of unit -> 'a |
+ Expr of Document_ID.exec * (unit -> 'a) |
Result of 'a Exn.result;
abstype 'a memo = Memo of 'a expr Synchronized.var
with
-fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
+fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
-fun memo_eval (Memo v) =
- (case Synchronized.value v of
- Result res => res
- | _ =>
- Synchronized.guarded_access v
- (fn Result res => SOME (res, Result res)
- | Expr e =>
- let val res = Exn.capture e (); (*sic!*)
- in SOME (res, Result res) end))
- |> Exn.release;
-
-fun memo_fork params (Memo v) =
- (case Synchronized.value v of
- Result _ => ()
- | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
-
fun memo_result (Memo v) =
(case Synchronized.value v of
- Result res => Exn.release res
- | _ => raise Fail "Unfinished memo result");
+ Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
+ | Result res => Exn.release res);
fun memo_stable (Memo v) =
(case Synchronized.value v of
- Expr _ => true
- | Result res => not (Exn.is_interrupt_exn res));
+ Expr _ => true
+ | Result res => not (Exn.is_interrupt_exn res));
+
+fun memo_exec execution_id (Memo v) =
+ Synchronized.guarded_access v
+ (fn expr =>
+ (case expr of
+ Result res => SOME (res, expr)
+ | Expr (exec_id, e) =>
+ uninterruptible (fn restore_attributes => fn () =>
+ if Execution.running execution_id exec_id then
+ let
+ val res = Exn.capture (restore_attributes e) ();
+ val _ = Execution.finished exec_id;
+ in SOME (res, Result res) end
+ else SOME (Exn.interrupt_exn, expr)) ()))
+ |> Exn.release |> ignore;
+
+fun memo_fork params execution_id (Memo v) =
+ (case Synchronized.value v of
+ Result _ => ()
+ | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
end;
@@ -76,46 +75,6 @@
(** main phases of execution **)
-(* basic type definitions *)
-
-type eval_state =
- {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
-val init_eval_state =
- {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
-
-type eval_process = eval_state memo;
-type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
-
-fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
-val eval_result_state = #state o eval_result;
-
-type print_process = unit memo;
-type print =
- {name: string, pri: int, persistent: bool,
- exec_id: Document_ID.exec, print_process: print_process};
-
-type exec = eval * print list;
-val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
-
-fun exec_ids (NONE: exec option) = []
- | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
-
-
-(* stable results *)
-
-fun stable_goals exec_id =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
-
-fun stable_eval ({exec_id, eval_process}: eval) =
- stable_goals exec_id andalso memo_stable eval_process;
-
-fun stable_print ({exec_id, print_process, ...}: print) =
- stable_goals exec_id andalso memo_stable print_process;
-
-fun same_eval (eval: eval, eval': eval) =
- #exec_id eval = #exec_id eval' andalso stable_eval eval';
-
-
(* read *)
fun read init span =
@@ -148,6 +107,21 @@
(* eval *)
+type eval_state =
+ {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
+val init_eval_state =
+ {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+
+datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
+
+fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
+
+fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
+val eval_result_state = #state o eval_result;
+
+fun eval_stable (Eval {exec_id, eval_process}) =
+ Goal.stable_futures exec_id andalso memo_stable eval_process;
+
local
fun run int tr st =
@@ -208,13 +182,17 @@
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
(fn () => read init span |> Toplevel.exec_id exec_id) ();
in eval_state span tr (eval_result eval0) end;
- in {exec_id = exec_id, eval_process = memo process} end;
+ in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
end;
(* print *)
+datatype print = Print of
+ {name: string, pri: int, persistent: bool,
+ exec_id: Document_ID.exec, print_process: unit memo};
+
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
local
@@ -226,6 +204,13 @@
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
+
+fun print_stable (Print {exec_id, print_process, ...}) =
+ Goal.stable_futures exec_id andalso memo_stable print_process;
+
+fun print_persistent (Print {persistent, ...}) = persistent;
+
in
fun print command_visible command_name eval old_prints =
@@ -244,8 +229,9 @@
else print_error tr (fn () => print_fn tr st')
end;
in
- {name = name, pri = pri, persistent = persistent,
- exec_id = exec_id, print_process = memo process}
+ Print {
+ name = name, pri = pri, persistent = persistent,
+ exec_id = exec_id, print_process = memo exec_id process}
end;
in
(case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
@@ -257,13 +243,12 @@
val new_prints =
if command_visible then
rev (Synchronized.value print_functions) |> map_filter (fn pr =>
- (case find_first (equal (fst pr) o #name) old_prints of
- SOME print => if stable_print print then SOME print else new_print pr
+ (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
+ SOME print => if print_stable print then SOME print else new_print pr
| NONE => new_print pr))
- else filter (fn print => #persistent print andalso stable_print print) old_prints;
+ else filter (fn print => print_persistent print andalso print_stable print) old_prints;
in
- if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
- else SOME new_prints
+ if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
end;
fun print_function {name, pri, persistent} f =
@@ -289,15 +274,29 @@
in if do_print then Toplevel.print_state false st' else () end));
-(* overall execution process *)
+(* combined execution *)
+
+type exec = eval * print list;
+val no_exec: exec =
+ (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
-fun run_print ({name, pri, print_process, ...}: print) =
+fun exec_ids NONE = []
+ | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
+ exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
+
+local
+
+fun run_print execution_id (Print {name, pri, print_process, ...}) =
(if Multithreading.enabled () then
memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
- else memo_eval) print_process;
+ else memo_exec) execution_id print_process;
-fun execute (({eval_process, ...}, prints): exec) =
- (memo_eval eval_process; List.app run_print prints);
+in
+
+fun exec execution_id (Eval {eval_process, ...}, prints) =
+ (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
end;
+end;
+
--- a/src/Pure/PIDE/document.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jul 12 13:12:21 2013 +0200
@@ -18,8 +18,6 @@
val init_state: state
val define_command: Document_ID.command -> string -> string -> state -> state
val remove_versions: Document_ID.version list -> state -> state
- val discontinue_execution: state -> unit
- val cancel_execution: state -> unit
val start_execution: state -> unit
val timing: bool Unsynchronized.ref
val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -110,7 +108,7 @@
fun changed_result node node' =
(case (get_result node, get_result node') of
- (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
+ (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
| (NONE, NONE) => false
| _ => true);
@@ -205,15 +203,10 @@
(** main state -- document structure and execution process **)
-type execution =
- {version_id: Document_ID.version,
- group: Future.group,
- running: bool Unsynchronized.ref};
+type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
-val no_execution =
- {version_id = Document_ID.none,
- group = Future.new_group NONE,
- running = Unsynchronized.ref false};
+val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
+fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
@@ -240,10 +233,7 @@
let
val versions' = Inttab.update_new (version_id, version) versions
handle Inttab.DUP dup => err_dup "document version" dup;
- val execution' =
- {version_id = version_id,
- group = Future.new_group NONE,
- running = Unsynchronized.ref true};
+ val execution' = next_execution version_id;
in (versions', commands, execution') end);
fun the_version (State {versions, ...}) version_id =
@@ -302,32 +292,30 @@
in (versions', commands', execution) end);
-
-(** document execution **)
-
-val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
-val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
-val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
+(* document execution *)
fun start_execution state =
let
- val {version_id, group, running} = execution_of state;
+ val {version_id, execution_id} = execution_of state;
val _ =
- if not (! running) orelse Task_Queue.is_canceled group then []
- else
+ if Execution.is_running execution_id then
nodes_of (the_version state version_id) |> String_Graph.schedule
(fn deps => fn (name, node) =>
if not (visible_node node) andalso finished_theory node then
Future.value ()
else
(singleton o Future.forks)
- {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
+ {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
(fn () =>
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
- SOME exec => if ! running then SOME (Command.execute exec) else NONE
- | NONE => NONE)) node ()));
+ SOME exec =>
+ if Execution.is_running execution_id
+ then SOME (Command.exec execution_id exec)
+ else NONE
+ | NONE => NONE)) node ()))
+ else [];
in () end;
@@ -413,7 +401,8 @@
val flags' = update_flags prev flags;
val same' =
(case (lookup_entry node0 command_id, opt_exec) of
- (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
+ (SOME (eval0, _), SOME (eval, _)) =>
+ Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
| _ => false);
val assign_update' = assign_update |> same' ?
(case opt_exec of
@@ -454,6 +443,11 @@
val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
val init' = if Keyword.is_theory_begin command_name then NONE else init;
in SOME (assign_update', (command_id', (eval', prints')), init') end;
+
+fun cancel_old_execs node0 (command_id, exec_ids) =
+ subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
+ |> map_filter (Execution.peek #> Option.map (tap Future.cancel_group));
+
in
fun update old_version_id new_version_id edits state =
@@ -464,7 +458,6 @@
val nodes = nodes_of new_version;
val is_required = make_required nodes;
- val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
val updated = timeit "Document.update" (fn () =>
nodes |> String_Graph.schedule
(fn deps => fn (name, node) =>
@@ -474,7 +467,7 @@
(fn () =>
let
val imports = map (apsnd Future.join) deps;
- val imports_changed = exists (#3 o #1 o #2) imports;
+ val imports_changed = exists (#4 o #1 o #2) imports;
val node_required = is_required name;
in
if imports_changed orelse AList.defined (op =) edits name orelse
@@ -513,22 +506,29 @@
if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
else SOME eval';
+ val assign_update = assign_update_result assigned_execs;
+ val old_groups = maps (cancel_old_execs node0) assign_update;
+
val node' = node
|> assign_update_apply assigned_execs
|> entries_stable (assign_update_null updated_execs)
|> set_result result;
val assigned_node = SOME (name, node');
val result_changed = changed_result node0 node';
- in
- ((assign_update_result assigned_execs, assigned_node, result_changed), node')
- end
- else (([], NONE, false), node)
+ in ((assign_update, old_groups, assigned_node, result_changed), node') end
+ else (([], [], NONE, false), node)
end))
|> Future.joins |> map #1);
+ val assign_update = maps #1 updated;
+ val old_groups = maps #2 updated;
+ val assigned_nodes = map_filter #3 updated;
+
val state' = state
- |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
- in (maps #1 updated, state') end;
+ |> define_version new_version_id (fold put_node assigned_nodes new_version);
+
+ val _ = timeit "Document.terminate" (fn () => List.app Future.terminate old_groups);
+ in (assign_update, state') end;
end;
--- a/src/Pure/PIDE/document_id.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/PIDE/document_id.ML Fri Jul 12 13:12:21 2013 +0200
@@ -12,6 +12,7 @@
type version = generic
type command = generic
type exec = generic
+ type execution = generic
val none: generic
val make: unit -> generic
val parse: string -> generic
@@ -25,6 +26,7 @@
type version = generic;
type command = generic;
type exec = generic;
+type execution = generic;
val none = 0;
val make = Counter.make ();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/execution.ML Fri Jul 12 13:12:21 2013 +0200
@@ -0,0 +1,68 @@
+(* Title: Pure/PIDE/execution.ML
+ Author: Makarius
+
+Global management of execution. Unique running execution serves as
+barrier for further exploration of exec fragments.
+*)
+
+signature EXECUTION =
+sig
+ val start: unit -> Document_ID.execution
+ val discontinue: unit -> unit
+ val is_running: Document_ID.execution -> bool
+ val running: Document_ID.execution -> Document_ID.exec -> bool
+ val finished: Document_ID.exec -> unit
+ val peek: Document_ID.exec -> Future.group option
+ val snapshot: unit -> Future.group list
+end;
+
+structure Execution: EXECUTION =
+struct
+
+val state =
+ Synchronized.var "Execution.state"
+ (Document_ID.none, Inttab.empty: Future.group Inttab.table);
+
+
+(* unique running execution *)
+
+fun start () =
+ let
+ val execution_id = Document_ID.make ();
+ val _ = Synchronized.change state (apfst (K execution_id));
+ in execution_id end;
+
+fun discontinue () =
+ Synchronized.change state (apfst (K Document_ID.none));
+
+fun is_running execution_id = execution_id = fst (Synchronized.value state);
+
+
+(* registered execs *)
+
+fun running execution_id exec_id =
+ Synchronized.guarded_access state
+ (fn (execution_id', execs) =>
+ let
+ val continue = execution_id = execution_id';
+ val execs' =
+ if continue then
+ Inttab.update_new (exec_id, Future.the_worker_group ()) execs
+ handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
+ else execs;
+ in SOME (continue, (execution_id', execs')) end);
+
+fun finished exec_id =
+ Synchronized.change state
+ (apsnd (fn execs =>
+ Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
+ error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
+
+fun peek exec_id =
+ Inttab.lookup (snd (Synchronized.value state)) exec_id;
+
+fun snapshot () =
+ Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
+
+end;
+
--- a/src/Pure/PIDE/protocol.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Jul 12 13:12:21 2013 +0200
@@ -17,17 +17,23 @@
val _ =
Isabelle_Process.protocol_command "Document.discontinue_execution"
- (fn [] => Document.discontinue_execution (Document.state ()));
+ (fn [] => Execution.discontinue ());
val _ =
Isabelle_Process.protocol_command "Document.cancel_execution"
- (fn [] => Document.cancel_execution (Document.state ()));
+ (fn [] =>
+ let
+ val _ = Execution.discontinue ();
+ val groups = Execution.snapshot ();
+ val _ = List.app Future.cancel_group groups;
+ val _ = List.app Future.terminate groups;
+ in () end);
val _ =
Isabelle_Process.protocol_command "Document.update"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
- val _ = Document.cancel_execution state;
+ val _ = Execution.discontinue ();
val old_id = Document_ID.parse old_id_string;
val new_id = Document_ID.parse new_id_string;
@@ -51,16 +57,17 @@
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
- val (assignment, state') = Document.update old_id new_id edits state;
+ val (assign_update, state') = Document.update old_id new_id edits state;
+
+ val _ = List.app Future.cancel_group (Goal.reset_futures ());
+ val _ = Isabelle_Process.reset_tracing ();
+
val _ =
Output.protocol_message Markup.assign_update
- ((new_id, assignment) |>
+ ((new_id, assign_update) |>
let open XML.Encode
in pair int (list (pair int (list int))) end
|> YXML.string_of_body);
-
- val _ = List.app Future.cancel_group (Goal.reset_futures ());
- val _ = Isabelle_Process.reset_tracing ();
val _ =
Event_Timer.request (Time.+ (Time.now (), seconds 0.02))
(fn () => Document.start_execution state');
--- a/src/Pure/ROOT Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/ROOT Fri Jul 12 13:12:21 2013 +0200
@@ -153,6 +153,7 @@
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/document_id.ML"
+ "PIDE/execution.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/xml.ML"
--- a/src/Pure/ROOT.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 12 13:12:21 2013 +0200
@@ -267,6 +267,7 @@
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
+use "PIDE/execution.ML";
use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";
--- a/src/Pure/goal.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Pure/goal.ML Fri Jul 12 13:12:21 2013 +0200
@@ -27,7 +27,8 @@
val norm_result: thm -> thm
val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
val fork: int -> (unit -> 'a) -> 'a future
- val peek_futures: serial -> unit future list
+ val peek_futures: int -> unit future list
+ val stable_futures: int-> bool
val reset_futures: unit -> Future.group list
val shutdown_futures: unit -> unit
val skip_proofs_enabled: unit -> bool
@@ -181,6 +182,9 @@
fun peek_futures id =
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
+fun stable_futures id =
+ not (Par_Exn.is_interrupted (Future.join_results (peek_futures id)));
+
fun reset_futures () =
Synchronized.change_result forked_proofs (fn (_, groups, _) =>
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));