1.1 --- a/src/Pure/PIDE/command.ML Tue Sep 03 01:12:40 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Tue Sep 03 11:29:01 2013 +0200
1.3 @@ -57,7 +57,7 @@
1.4 (case expr of
1.5 Expr (exec_id, body) =>
1.6 uninterruptible (fn restore_attributes => fn () =>
1.7 - if Execution.running execution_id exec_id then
1.8 + if Execution.running execution_id exec_id [Future.the_worker_group ()] then
1.9 let
1.10 val res =
1.11 (body
2.1 --- a/src/Pure/PIDE/execution.ML Tue Sep 03 01:12:40 2013 +0200
2.2 +++ b/src/Pure/PIDE/execution.ML Tue Sep 03 11:29:01 2013 +0200
2.3 @@ -11,7 +11,7 @@
2.4 val discontinue: unit -> unit
2.5 val is_running: Document_ID.execution -> bool
2.6 val is_running_exec: Document_ID.exec -> bool
2.7 - val running: Document_ID.execution -> Document_ID.exec -> bool
2.8 + val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
2.9 val peek: Document_ID.exec -> Future.group list
2.10 val cancel: Document_ID.exec -> unit
2.11 val terminate: Document_ID.exec -> unit
2.12 @@ -33,7 +33,7 @@
2.13 fun make_state (execution, execs) = State {execution = execution, execs = execs};
2.14 fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
2.15
2.16 -val init_state = make_state (Document_ID.none, Inttab.empty);
2.17 +val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
2.18 val state = Synchronized.var "Execution.state" init_state;
2.19
2.20 fun get_state () = let val State args = Synchronized.value state in args end;
2.21 @@ -58,18 +58,18 @@
2.22 fun is_running_exec exec_id =
2.23 Inttab.defined (#execs (get_state ())) exec_id;
2.24
2.25 -fun running execution_id exec_id =
2.26 - Synchronized.guarded_access state
2.27 +fun running execution_id exec_id groups =
2.28 + Synchronized.change_result state
2.29 (fn State {execution = execution_id', execs} =>
2.30 let
2.31 val continue = execution_id = execution_id';
2.32 val execs' =
2.33 if continue then
2.34 - Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
2.35 + Inttab.update_new (exec_id, groups) execs
2.36 handle Inttab.DUP dup =>
2.37 - error ("Execution already registered: " ^ Document_ID.print dup)
2.38 + raise Fail ("Execution already registered: " ^ Document_ID.print dup)
2.39 else execs;
2.40 - in SOME (continue, make_state (execution_id', execs')) end);
2.41 + in (continue, make_state (execution_id', execs')) end);
2.42
2.43 fun peek exec_id =
2.44 Inttab.lookup_list (#execs (get_state ())) exec_id;
2.45 @@ -89,7 +89,10 @@
2.46 let
2.47 val exec_id = the_default 0 (Position.parse_id pos);
2.48 val group = Future.worker_subgroup ();
2.49 - val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
2.50 + val _ = change_state (apsnd (fn execs =>
2.51 + if Inttab.defined execs exec_id
2.52 + then Inttab.cons_list (exec_id, group) execs
2.53 + else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
2.54
2.55 val future =
2.56 (singleton o Future.forks)
2.57 @@ -127,7 +130,7 @@
2.58 if Inttab.defined execs' exec_id then ()
2.59 else groups |> List.app (fn group =>
2.60 if Task_Queue.is_canceled group then ()
2.61 - else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
2.62 + else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
2.63 in execs' end);
2.64
2.65 fun reset () =
3.1 --- a/src/Pure/Thy/thy_info.ML Tue Sep 03 01:12:40 2013 +0200
3.2 +++ b/src/Pure/Thy/thy_info.ML Tue Sep 03 11:29:01 2013 +0200
3.3 @@ -165,18 +165,20 @@
3.4 (* scheduling loader tasks *)
3.5
3.6 datatype result =
3.7 - Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
3.8 + Result of {theory: theory, exec_id: Document_ID.exec,
3.9 + present: unit -> unit, commit: unit -> unit, weight: int};
3.10
3.11 -fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
3.12 +fun theory_result theory =
3.13 + Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
3.14
3.15 fun result_theory (Result {theory, ...}) = theory;
3.16 fun result_present (Result {present, ...}) = present;
3.17 fun result_commit (Result {commit, ...}) = commit;
3.18 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
3.19
3.20 -fun join_theory (Result {theory, id, ...}) =
3.21 +fun join_theory (Result {theory, exec_id, ...}) =
3.22 Exn.capture Thm.join_theory_proofs theory ::
3.23 - map Exn.Exn (maps Task_Queue.group_status (Execution.peek id));
3.24 + map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
3.25
3.26
3.27 datatype task =
3.28 @@ -271,13 +273,19 @@
3.29
3.30 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
3.31
3.32 - val id = serial ();
3.33 - val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
3.34 + val exec_id = Document_ID.make ();
3.35 + val _ =
3.36 + Execution.running Document_ID.none exec_id [] orelse
3.37 + raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
3.38 +
3.39 + val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
3.40 val (theory, present, weight) =
3.41 Thy_Load.load_thy last_timing update_time dir header text_pos text
3.42 (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
3.43 fun commit () = update_thy deps theory;
3.44 - in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
3.45 + in
3.46 + Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
3.47 + end;
3.48
3.49 fun check_deps dir name =
3.50 (case lookup_deps name of