# HG changeset patch # User wenzelm # Date 1378200541 -7200 # Node ID 78693e46a2378d527379a49d0ed80d5f589a5536 # Parent a14d2a854c0241b418ec7b7dd6c31dc026e7f61c Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document); diff -r a14d2a854c02 -r 78693e46a237 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Sep 03 01:12:40 2013 +0200 +++ b/src/Pure/PIDE/command.ML Tue Sep 03 11:29:01 2013 +0200 @@ -57,7 +57,7 @@ (case expr of Expr (exec_id, body) => uninterruptible (fn restore_attributes => fn () => - if Execution.running execution_id exec_id then + if Execution.running execution_id exec_id [Future.the_worker_group ()] then let val res = (body diff -r a14d2a854c02 -r 78693e46a237 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Tue Sep 03 01:12:40 2013 +0200 +++ b/src/Pure/PIDE/execution.ML Tue Sep 03 11:29:01 2013 +0200 @@ -11,7 +11,7 @@ val discontinue: unit -> unit val is_running: Document_ID.execution -> bool val is_running_exec: Document_ID.exec -> bool - val running: Document_ID.execution -> Document_ID.exec -> bool + val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool val peek: Document_ID.exec -> Future.group list val cancel: Document_ID.exec -> unit val terminate: Document_ID.exec -> unit @@ -33,7 +33,7 @@ fun make_state (execution, execs) = State {execution = execution, execs = execs}; fun map_state f (State {execution, execs}) = make_state (f (execution, execs)); -val init_state = make_state (Document_ID.none, Inttab.empty); +val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]); val state = Synchronized.var "Execution.state" init_state; fun get_state () = let val State args = Synchronized.value state in args end; @@ -58,18 +58,18 @@ fun is_running_exec exec_id = Inttab.defined (#execs (get_state ())) exec_id; -fun running execution_id exec_id = - Synchronized.guarded_access state +fun running execution_id exec_id groups = + Synchronized.change_result state (fn State {execution = 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 + Inttab.update_new (exec_id, groups) execs handle Inttab.DUP dup => - error ("Execution already registered: " ^ Document_ID.print dup) + raise Fail ("Execution already registered: " ^ Document_ID.print dup) else execs; - in SOME (continue, make_state (execution_id', execs')) end); + in (continue, make_state (execution_id', execs')) end); fun peek exec_id = Inttab.lookup_list (#execs (get_state ())) exec_id; @@ -89,7 +89,10 @@ let val exec_id = the_default 0 (Position.parse_id pos); val group = Future.worker_subgroup (); - val _ = change_state (apsnd (Inttab.cons_list (exec_id, group))); + val _ = change_state (apsnd (fn execs => + if Inttab.defined execs exec_id + then Inttab.cons_list (exec_id, group) execs + else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id))); val future = (singleton o Future.forks) @@ -127,7 +130,7 @@ if Inttab.defined execs' exec_id then () else groups |> List.app (fn group => if Task_Queue.is_canceled group then () - else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id))); + else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id))); in execs' end); fun reset () = diff -r a14d2a854c02 -r 78693e46a237 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Sep 03 01:12:40 2013 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Sep 03 11:29:01 2013 +0200 @@ -165,18 +165,20 @@ (* scheduling loader tasks *) datatype result = - Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int}; + Result of {theory: theory, exec_id: Document_ID.exec, + present: unit -> unit, commit: unit -> unit, weight: int}; -fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0}; +fun theory_result theory = + Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; fun result_present (Result {present, ...}) = present; fun result_commit (Result {commit, ...}) = commit; fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); -fun join_theory (Result {theory, id, ...}) = +fun join_theory (Result {theory, exec_id, ...}) = Exn.capture Thm.join_theory_proofs theory :: - map Exn.Exn (maps Task_Queue.group_status (Execution.peek id)); + map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)); datatype task = @@ -271,13 +273,19 @@ val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); - val id = serial (); - val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path); + val exec_id = Document_ID.make (); + val _ = + Execution.running Document_ID.none exec_id [] orelse + raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); + + val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = Thy_Load.load_thy last_timing update_time dir header text_pos text (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); fun commit () = update_thy deps theory; - in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end; + in + Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} + end; fun check_deps dir name = (case lookup_deps name of