# HG changeset patch # User wenzelm # Date 1361904266 -3600 # Node ID 59a03019f3bfe4da6795163ff37e007001b8c58a # Parent fefd0769797918b582d623dd50922306a36bd627 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; diff -r fefd07697979 -r 59a03019f3bf src/Pure/Isar/toplevel.ML --- 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' diff -r fefd07697979 -r 59a03019f3bf src/Pure/PIDE/command.ML --- 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 diff -r fefd07697979 -r 59a03019f3bf src/Pure/Thy/thy_info.ML --- 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