# HG changeset patch # User wenzelm # Date 1373627541 -7200 # Node ID 78a64edf431fa2cd66823ba4ed7b044f0d3b2dc0 # Parent 8afb396d9178c9524b69f6962f2be59b505157cd# Parent c8f8c29193def05f166a02c85691ceaad6d1a51b merged diff -r 8afb396d9178 -r 78a64edf431f src/HOL/Hoare_Parallel/Gar_Coll.thy --- 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)+ diff -r 8afb396d9178 -r 78a64edf431f src/HOL/Hoare_Parallel/OG_Tactics.thy --- 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. \(b x)}" -by fast -lemma list_length: "length []=0 \ length (x#xs) = Suc(length xs)" -by simp -lemma list_lemmas: "length []=0 \ length (x#xs) = Suc(length xs) -\ (x#xs) ! 0=x \ (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 ('a \ 'a) set \ bool" where "stable \ \f g. (\x y. x \ f \ (x, y) \ g \ y \ 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\ cptn_mod \ \s P. x !0=(Some (Seq P Q), s) \ (\iSome Q) \ @@ -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 \ cptn \ \s P i. x!0=(Some (Seq P Q), s) \ i_i"} at step @{text "m"}. *} apply(drule_tac n=j and P="\j. \i. ?H i j" in Ex_first_occurrence) @@ -1128,7 +1125,7 @@ apply clarify apply(erule_tac x=m and P="\j. ?I j \ ?J j \ ?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="\j. ?H j \ ?I j \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="\j. ?H j \ ?M \ UNION (?S j) (?T j) \ (?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 \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); Suc i < length x; x ! i -pc\ x ! Suc i\ \ (snd (x ! i), snd (x ! Suc i)) \ guar" -apply(simp add: ParallelCom_def del: Un_subset_iff) +apply(simp add: ParallelCom_def) apply(subgoal_tac "(map (Some \ fst) xs)\[]") 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 @@ \ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; x \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); All_None (fst (last x)) \ \ snd (last x) \ post" -apply(simp add: ParallelCom_def del: Un_subset_iff) +apply(simp add: ParallelCom_def) apply(subgoal_tac "(map (Some \ fst) xs)\[]") 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 "\iassum(Pre(xs!i), Rely(xs!i))") apply(erule_tac x=i and P="\i. ?H i \ \ (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption) diff -r 8afb396d9178 -r 78a64edf431f src/Pure/Concurrent/future.ML --- 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; diff -r 8afb396d9178 -r 78a64edf431f src/Pure/PIDE/command.ML --- 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; + diff -r 8afb396d9178 -r 78a64edf431f src/Pure/PIDE/document.ML --- 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; diff -r 8afb396d9178 -r 78a64edf431f src/Pure/PIDE/document_id.ML --- 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 (); diff -r 8afb396d9178 -r 78a64edf431f src/Pure/PIDE/execution.ML --- /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; + diff -r 8afb396d9178 -r 78a64edf431f src/Pure/PIDE/protocol.ML --- 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'); diff -r 8afb396d9178 -r 78a64edf431f src/Pure/ROOT --- 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" diff -r 8afb396d9178 -r 78a64edf431f src/Pure/ROOT.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"; diff -r 8afb396d9178 -r 78a64edf431f src/Pure/goal.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))));