# HG changeset patch # User wenzelm # Date 1350567854 -7200 # Node ID 18af317f393aef21f35b796b73fc4552c7dbc0c8 # Parent 26a0263f9f4681ddc9a5ad20e9c35f396de72df7# Parent 12cece6d951da368db249841da93f35b06ba4e4b merged diff -r 26a0263f9f46 -r 18af317f393a src/HOL/Cardinals/Wellorder_Embedding_Base.thy --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 15:40:02 2012 +0200 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Oct 18 15:44:14 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) \ (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 \ 'a' * bool" and f::"'a \ 'a'" and g::"'a \ bool" diff -r 26a0263f9f46 -r 18af317f393a src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Oct 18 15:40:02 2012 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Oct 18 15:44:14 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); diff -r 26a0263f9f46 -r 18af317f393a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Oct 18 15:40:02 2012 +0200 +++ b/src/Pure/Isar/proof.ML Thu Oct 18 15:44:14 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 diff -r 26a0263f9f46 -r 18af317f393a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Oct 18 15:40:02 2012 +0200 +++ b/src/Pure/PIDE/document.ML Thu Oct 18 15:44:14 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 diff -r 26a0263f9f46 -r 18af317f393a src/Pure/System/build.ML --- a/src/Pure/System/build.ML Thu Oct 18 15:40:02 2012 +0200 +++ b/src/Pure/System/build.ML Thu Oct 18 15:44:14 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); diff -r 26a0263f9f46 -r 18af317f393a src/Pure/System/session.ML --- a/src/Pure/System/session.ML Thu Oct 18 15:40:02 2012 +0200 +++ b/src/Pure/System/session.ML Thu Oct 18 15:44:14 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