--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 13:19:44 2012 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 15:16:39 2012 +0200
@@ -722,8 +722,8 @@
(snd o h1) y = (snd o h2) y" by auto
hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
(snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
- by (auto simp add: image_def)
- thus "H h1 x = H h2 x" by (simp add: H_def)
+ by (auto simp add: image_def)
+ thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
qed
(* More constant definitions: *)
obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
--- a/src/Pure/Concurrent/future.ML Thu Oct 18 13:19:44 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Oct 18 15:16:39 2012 +0200
@@ -26,10 +26,10 @@
* Future tasks are organized in groups, which are block-structured.
When forking a new new task, the default is to open an individual
subgroup, unless some common group is specified explicitly.
- Failure of one group member causes the immediate peers to be
- interrupted eventually (i.e. none by default). Interrupted tasks
- that lack regular result information, will pick up parallel
- exceptions from the cumulative group context (as Par_Exn).
+ Failure of one group member causes peer and subgroup members to be
+ interrupted eventually. Interrupted tasks that lack regular
+ result information, will pick up parallel exceptions from the
+ cumulative group context (as Par_Exn).
* Future task groups may be canceled: present and future group
members will be interrupted eventually.
@@ -63,7 +63,6 @@
val join_result: 'a future -> 'a Exn.result
val joins: 'a future list -> 'a list
val join: 'a future -> 'a
- val join_tasks: task list -> unit
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
val cond_forks: params -> (unit -> 'a) list -> 'a future list
@@ -72,9 +71,8 @@
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
+ val terminate: group -> unit
val shutdown: unit -> unit
- val group_tasks: group -> task list
- val queue_status: unit -> {ready: int, pending: int, running: int, passive: int}
end;
structure Future: FUTURE =
@@ -410,12 +408,15 @@
(* cancel *)
-fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+fun cancel_group_unsynchronized group = (*requires SYNCHRONIZED*)
let
val _ = if null (cancel_now group) then () else cancel_later group;
val _ = signal work_available;
val _ = scheduler_check ();
- in () end);
+ in () end;
+
+fun cancel_group group =
+ SYNCHRONIZED "cancel_group" (fn () => cancel_group_unsynchronized group);
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
@@ -542,13 +543,6 @@
fun joins xs = Par_Exn.release_all (join_results xs);
fun join x = Exn.release (join_result x);
-fun join_tasks [] = ()
- | join_tasks tasks =
- (singleton o forks)
- {name = "join_tasks", group = SOME (new_group NONE),
- deps = tasks, pri = 0, interrupts = false} I
- |> join;
-
(* fast-path versions -- bypassing task queue *)
@@ -569,7 +563,7 @@
fun map_future f x =
let
val task = task_of x;
- val group = new_group (SOME (Task_Queue.group_of_task task));
+ val group = Task_Queue.group_of_task task;
val (result, job) = future_job group true (fn () => f (join x));
val extended = SYNCHRONIZED "extend" (fn () =>
@@ -633,6 +627,24 @@
fun fulfill x res = fulfill_result x (Exn.Res res);
+(* terminate *)
+
+fun terminate group =
+ let
+ val tasks =
+ SYNCHRONIZED "terminate" (fn () =>
+ let val _ = cancel_group_unsynchronized group;
+ in Task_Queue.group_tasks (! queue) group end);
+ in
+ if null tasks then ()
+ else
+ (singleton o forks)
+ {name = "terminate", group = SOME (new_group NONE),
+ deps = tasks, pri = 0, interrupts = false} I
+ |> join
+ end;
+
+
(* shutdown *)
fun shutdown () =
@@ -645,8 +657,6 @@
(* queue status *)
-fun group_tasks group = Task_Queue.group_tasks (! queue) group;
-
fun queue_status () = Task_Queue.status (! queue);
--- a/src/Pure/Isar/proof.ML Thu Oct 18 13:19:44 2012 +0200
+++ b/src/Pure/Isar/proof.ML Thu Oct 18 15:16:39 2012 +0200
@@ -339,8 +339,10 @@
fun pretty_facts _ _ NONE = []
| pretty_facts s ctxt (SOME ths) =
[(Pretty.block o Pretty.fbreaks)
- (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] ::
- map (Display.pretty_thm ctxt) ths), Pretty.str ""];
+ ((if s = "" then Pretty.str "this:"
+ else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
+ map (Display.pretty_thm ctxt) ths),
+ Pretty.str ""];
fun pretty_state nr state =
let
@@ -349,7 +351,7 @@
fun prt_goal (SOME (_, (_,
{statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
- pretty_facts "using " ctxt
+ pretty_facts "using" ctxt
(if mode <> Backward orelse null using then NONE else SOME using) @
[Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
@@ -366,7 +368,7 @@
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
- else if mode = Chain then pretty_facts "picking " ctxt facts
+ else if mode = Chain then pretty_facts "picking" ctxt facts
else prt_goal (try find_goal state))
end;
@@ -1000,7 +1002,7 @@
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
-(* concluding steps *)
+(* terminal proof steps *)
local
@@ -1008,28 +1010,42 @@
proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
#> Seq.the_result "";
-fun skipped_proof x =
- (Output.report (Markup.markup Isabelle_Markup.bad "Skipped proof"); x);
-
in
fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
-fun local_skip_proof int =
- local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
-fun global_skip_proof int =
- global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
end;
+(* skip proofs *)
+
+local
+
+fun skipped_proof state =
+ Context_Position.if_visible (context_of state) Output.report
+ (Markup.markup Isabelle_Markup.bad "Skipped proof");
+
+in
+
+fun local_skip_proof int state =
+ local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
+ skipped_proof state;
+
+fun global_skip_proof int state =
+ global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
+ skipped_proof state;
+
+end;
+
+
(* common goal statements *)
local
@@ -1069,7 +1085,7 @@
state
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
|> int ? (fn goal_state =>
- (case test_proof goal_state of
+ (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
Exn.Res (SOME _) => goal_state
| Exn.Res NONE => error (fail_msg (context_of goal_state))
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
@@ -1109,6 +1125,21 @@
local
+structure Result = Proof_Data
+(
+ type T = thm option;
+ val empty = NONE;
+ fun init _ = empty;
+);
+
+fun the_result ctxt =
+ (case Result.get ctxt of
+ NONE => error "No result of forked proof"
+ | SOME th => th);
+
+val set_result = Result.put o SOME;
+val reset_result = Result.put NONE;
+
fun future_proof done get_context fork_proof state =
let
val _ = assert_backward state;
@@ -1124,20 +1155,16 @@
val statement' = (kind, [[], [prop']], prop');
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
-
- fun after_local' [[th]] = put_thms false (Auto_Bind.thisN, SOME [th]);
- fun after_global' [[th]] = Proof_Context.put_thms false (Auto_Bind.thisN, SOME [th]);
- val after_qed' = (after_local', after_global');
- val this_name = Proof_Context.full_name goal_ctxt (Binding.name Auto_Bind.thisN);
+ val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
val result_ctxt =
state
+ |> map_context reset_result
|> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
(fold (Variable.declare_typ o TFree) goal_tfrees)
|> fork_proof;
- val future_thm = result_ctxt |> Future.map (fn (_, x) =>
- Proof_Context.get_fact_single (get_context x) (Facts.named this_name));
+ val future_thm = result_ctxt |> Future.map (fn (_, x) => the_result (get_context x));
val finished_goal = Goal.future_result goal_ctxt future_thm prop';
val state' =
state
--- a/src/Pure/PIDE/document.ML Thu Oct 18 13:19:44 2012 +0200
+++ b/src/Pure/PIDE/document.ML Thu Oct 18 15:16:39 2012 +0200
@@ -318,14 +318,8 @@
(** document execution **)
val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
-
val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
-
-fun terminate_execution state =
- let
- val (_, group, _) = execution_of state;
- val _ = Future.cancel_group group;
- in Future.join_tasks (Future.group_tasks group) end;
+val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
fun start_execution state =
let
--- a/src/Pure/System/build.ML Thu Oct 18 13:19:44 2012 +0200
+++ b/src/Pure/System/build.ML Thu Oct 18 15:16:39 2012 +0200
@@ -88,13 +88,16 @@
(Options.string options "document_dump",
Present.dump_mode (Options.string options "document_dump_mode"))
"" verbose;
- val _ =
+
+ val res1 =
theories |>
(List.app use_theories
|> Session.with_timing name verbose
- |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads"));
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+ |> Exn.capture);
+ val res2 = Exn.capture Session.finish ();
+ val _ = Par_Exn.release_all [res1, res2];
- val _ = Session.finish ();
val _ = if do_output then () else exit 0;
in 0 end);
--- a/src/Pure/System/session.ML Thu Oct 18 13:19:44 2012 +0200
+++ b/src/Pure/System/session.ML Thu Oct 18 15:16:39 2012 +0200
@@ -67,16 +67,16 @@
(* finish *)
fun finish () =
- (Thy_Info.finish ();
- Present.finish ();
- Keyword.status ();
- Outer_Syntax.check_syntax ();
- Future.shutdown ();
- Goal.finish_futures ();
- Goal.cancel_futures ();
- Future.shutdown ();
- Options.reset_default ();
- session_finished := true);
+ (Future.shutdown ();
+ Goal.finish_futures ();
+ Thy_Info.finish ();
+ Present.finish ();
+ Keyword.status ();
+ Outer_Syntax.check_syntax ();
+ Goal.cancel_futures ();
+ Future.shutdown ();
+ Options.reset_default ();
+ session_finished := true);
(* use_dir *)
@@ -124,12 +124,16 @@
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
- (Output.physical_stderr
- "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
- init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
- (doc_dump dump) rpath verbose;
- with_timing item timing use root;
- finish ()))
+ let
+ val _ =
+ Output.physical_stderr
+ "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
+ val _ =
+ init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
+ (doc_dump dump) rpath verbose;
+ val res1 = (use |> with_timing item timing |> Exn.capture) root;
+ val res2 = Exn.capture finish ();
+ in ignore (Par_Exn.release_all [res1, res2]) end)
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs