--- a/src/Doc/Tutorial/ToyList/ToyList.thy Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Wed Feb 27 10:33:45 2013 +0100
@@ -3,13 +3,14 @@
begin
(*<*)
-ML {*
+ML {* (* FIXME somewhat non-standard, fragile *)
let
val texts =
map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
["ToyList1", "ToyList2"];
val trs = Outer_Syntax.parse Position.start (implode texts);
- in @{assert} (Toplevel.is_toplevel (fold Toplevel.command trs Toplevel.toplevel)) end;
+ val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
+ in @{assert} (Toplevel.is_toplevel end_state) end;
*}
(*>*)
--- a/src/HOL/Word/Word.thy Wed Feb 27 10:33:30 2013 +0100
+++ b/src/HOL/Word/Word.thy Wed Feb 27 10:33:45 2013 +0100
@@ -1644,11 +1644,10 @@
apply (erule (2) udvd_decr0)
done
-ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
-
lemma udvd_incr2_K:
"p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
+ using [[simproc del: linordered_ring_less_cancel_factor]]
apply (unfold udvd_def)
apply clarify
apply (simp add: uint_arith_simps split: split_if_asm)
@@ -1662,8 +1661,6 @@
apply simp
done
-ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
-
(* links with rbl operations *)
lemma word_succ_rbl:
"to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
--- a/src/Pure/Concurrent/future.ML Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Feb 27 10:33:45 2013 +0100
@@ -154,10 +154,6 @@
fun broadcast cond = (*requires SYNCHRONIZED*)
ConditionVar.broadcast cond;
-fun broadcast_work () = (*requires SYNCHRONIZED*)
- (ConditionVar.broadcast work_available;
- ConditionVar.broadcast work_finished);
-
end;
@@ -331,7 +327,7 @@
val _ = workers := alive;
in
Multithreading.tracing 0 (fn () =>
- "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
+ "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
end;
@@ -380,7 +376,7 @@
(Multithreading.tracing 1 (fn () =>
string_of_int (length (! canceled)) ^ " canceled groups");
Unsynchronized.change canceled (filter_out (null o cancel_now));
- broadcast_work ());
+ signal work_available);
(* delay loop *)
@@ -398,9 +394,9 @@
in continue end
handle exn =>
if Exn.is_interrupt exn then
- (Multithreading.tracing 1 (fn () => "Interrupt");
+ (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
List.app cancel_later (cancel_all ());
- broadcast_work (); true)
+ signal work_available; true)
else reraise exn;
fun scheduler_loop () =
@@ -682,11 +678,14 @@
(* shutdown *)
fun shutdown () =
- if Multithreading.available then
+ if not Multithreading.available then ()
+ else if is_some (worker_task ()) then
+ raise Fail "Cannot shutdown while running as worker thread"
+ else
SYNCHRONIZED "shutdown" (fn () =>
- while scheduler_active () do
- (wait scheduler_event; broadcast_work ()))
- else ();
+ while scheduler_active () do
+ (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
+ wait scheduler_event));
(*final declarations of this structure!*)
--- a/src/Pure/Isar/runtime.ML Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Feb 27 10:33:45 2013 +0100
@@ -12,7 +12,8 @@
exception TOPLEVEL_ERROR
val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
- val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
+ type error = ((serial * string) * string option)
+ val exn_messages_ids: (exn -> Position.T) -> exn -> error list
val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
@@ -43,6 +44,8 @@
(* exn_message *)
+type error = ((serial * string) * string option);
+
local
fun if_context NONE _ _ = []
--- a/src/Pure/Isar/toplevel.ML Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Feb 27 10:33:45 2013 +0100
@@ -94,7 +94,8 @@
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 command_exception: bool -> transition -> state -> state
+ val command_errors: bool -> transition -> state -> Runtime.error list * state option
val element_result: transition Thy_Syntax.element -> state ->
(transition * state) list future * state
end;
@@ -636,8 +637,7 @@
local
fun timing_message tr (t: Timing.timing) =
- if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
- then
+ if Timing.is_relevant_time (#elapsed t) then
(case approximative_id tr of
SOME id =>
(Output.protocol_message
@@ -685,15 +685,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 *)
@@ -704,12 +710,23 @@
fun init _ = empty;
);
+fun priority trs =
+ let val estimate = fold (curry Time.+ o get_timing) trs Time.zeroTime in
+ if estimate = Time.zeroTime then ~1
+ else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
+ end;
+
fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
let
- val future_enabled = Goal.future_enabled ();
+ val command = command_exception (! interact);
fun atom_result tr st =
- let val st' = command 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 =
@@ -717,9 +734,9 @@
NONE => []
| SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
- val st' = command head_tr st;
+ val (_, st') = atom_result head_tr st;
in
- if not future_enabled orelse is_ignored head_tr orelse
+ if not (Goal.future_enabled ()) orelse is_ignored head_tr orelse
null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
then
let val (results, st'') = fold_map atom_result proof_trs st'
@@ -729,20 +746,16 @@
val (body_trs, end_tr) = split_last proof_trs;
val finish = Context.Theory o Proof_Context.theory_of;
- val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
- val pri =
- if estimate = Time.zeroTime then ~1
- else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
-
val future_proof = Proof.global_future_proof
(fn prf =>
- Goal.fork_name "Toplevel.future_proof" pri
- (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/ML/ml_compiler.ML Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML Wed Feb 27 10:33:45 2013 +0100
@@ -7,7 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
- val exn_messages_ids: exn -> ((serial * string) * string option) list
+ val exn_messages_ids: exn -> Runtime.error list
val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
--- a/src/Pure/PIDE/command.ML Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/PIDE/command.ML Wed Feb 27 10:33:45 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 Wed Feb 27 10:33:30 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Feb 27 10:33:45 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