fork diagnostic commands (theory loader and PIDE interaction);
explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions;
clarified Toplevel.command_exception vs. Toplevel.command_errors;
--- a/src/Pure/Isar/toplevel.ML Tue Feb 26 13:38:34 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Feb 26 19:44:26 2013 +0100
@@ -94,8 +94,9 @@
val get_timing: transition -> Time.time
val put_timing: Time.time -> transition -> transition
val transition: bool -> transition -> state -> (state * (exn * string) option) option
- val command: transition -> state -> state
- val atom_result: transition -> state -> (transition * state) * state
+ val command_exception: bool -> transition -> state -> state
+ val command_errors: bool -> transition -> state ->
+ ((serial * string) * string option) list * state option
val element_result: transition Thy_Syntax.element -> state ->
(transition * state) list future * state
end;
@@ -685,15 +686,21 @@
end;
-(* nested commands *)
+(* managed commands *)
-fun command tr st =
- (case transition (! interact) tr st of
+fun command_exception int tr st =
+ (case transition int tr st of
SOME (st', NONE) => st'
| SOME (_, SOME (exn, info)) =>
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
| NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
+fun command_errors int tr st =
+ (case transition int tr st of
+ SOME (st', NONE) => ([], SOME st')
+ | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
+ | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
+
(* scheduled proof result *)
@@ -710,12 +717,19 @@
else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
end;
-fun atom_result tr st =
- let val st' = command tr st
- in ((tr, st'), st') end;
-
fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
let
+ val command = command_exception (! interact);
+
+ fun atom_result tr st =
+ let
+ val st' =
+ if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
+ setmp_thread_position tr (fn () =>
+ (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) ()
+ else command tr st;
+ in ((tr, st'), st') end;
+
val proof_trs =
(case opt_proof of
NONE => []
@@ -735,13 +749,14 @@
val future_proof = Proof.global_future_proof
(fn prf =>
- Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
- (fn () =>
- let val (result, result_state) =
- (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
- => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
- |> fold_map atom_result body_trs ||> command end_tr;
- in (result, presentation_context_of result_state) end))
+ setmp_thread_position head_tr (fn () =>
+ Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
+ (fn () =>
+ let val (result, result_state) =
+ (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+ => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
+ |> fold_map atom_result body_trs ||> command end_tr;
+ in (result, presentation_context_of result_state) end)) ())
#-> Result.put;
val st'' = st'
--- a/src/Pure/PIDE/command.ML Tue Feb 26 13:38:34 2013 +0100
+++ b/src/Pure/PIDE/command.ML Tue Feb 26 19:44:26 2013 +0100
@@ -62,10 +62,11 @@
local
fun run int tr st =
- (case Toplevel.transition int tr st of
- SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
- | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
+ if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
+ Toplevel.setmp_thread_position tr (fn () =>
+ (Goal.fork_name "Toplevel.diag" ~1
+ (fn () => Toplevel.command_exception int tr st); ([], SOME st))) ()
+ else Toplevel.command_errors int tr st;
fun check_cmts tr cmts st =
Toplevel.setmp_thread_position tr
--- a/src/Pure/Thy/thy_info.ML Tue Feb 26 13:38:34 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Feb 26 19:44:26 2013 +0100
@@ -164,7 +164,7 @@
(* scheduling loader tasks *)
-type result = theory * unit future * (unit -> unit);
+type result = theory * serial * unit future * (unit -> unit);
datatype task =
Task of string list * (theory list -> result) |
@@ -177,8 +177,14 @@
local
-fun finish_thy ((thy, present, commit): result) =
- (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
+fun finish_thy ((thy, id, present, commit): result) =
+ let
+ val result1 = Exn.capture Thm.join_theory_proofs thy;
+ val results2 = Future.join_results (Goal.peek_futures id);
+ val result3 = Future.join_result present;
+ val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
+ val _ = commit ();
+ in thy end;
val schedule_seq =
String_Graph.schedule (fn deps => fn (_, task) =>
@@ -186,22 +192,29 @@
Task (parents, body) => finish_thy (body (task_parents deps parents))
| Finished thy => thy)) #> ignore;
-val schedule_futures = uninterruptible (fn _ =>
- String_Graph.schedule (fn deps => fn (name, task) =>
- (case task of
- Task (parents, body) =>
- (singleton o Future.forks)
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
- (fn () =>
- (case filter (not o can Future.join o #2) deps of
- [] => body (map (#1 o Future.join) (task_parents deps parents))
- | bad =>
- error (loader_msg ("failed to load " ^ quote name ^
- " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
- | Finished thy => Future.value (thy, Future.value (), I)))
- #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
- #> rev #> Par_Exn.release_all) #> ignore;
+val schedule_futures = uninterruptible (fn _ => fn tasks =>
+ let
+ val results1 = tasks
+ |> String_Graph.schedule (fn deps => fn (name, task) =>
+ (case task of
+ Task (parents, body) =>
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
+ (fn () =>
+ (case filter (not o can Future.join o #2) deps of
+ [] => body (map (#1 o Future.join) (task_parents deps parents))
+ | bad =>
+ error (loader_msg ("failed to load " ^ quote name ^
+ " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
+ | Finished thy => Future.value (thy, 0, Future.value (), I)))
+ |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
+
+ (* FIXME avoid global reset_futures (!??) *)
+ val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
+
+ val _ = Par_Exn.release_all (rev (results2 @ results1));
+ in () end);
in
@@ -234,11 +247,13 @@
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 (theory, present) =
- Thy_Load.load_thy last_timing update_time dir header (Path.position thy_path) text
+ 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 (theory, present, commit) end;
+ in (theory, id, present, commit) end;
fun check_deps dir name =
(case lookup_deps name of