merged
authorwenzelm
Thu, 18 Oct 2012 15:44:14 +0200
changeset 49925 18af317f393a
parent 49920 26a0263f9f46 (current diff)
parent 49924 12cece6d951d (diff)
child 49926 a9f5a7496258
merged
--- 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) \<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 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);
 
 
--- 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
--- 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
--- 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);
 
--- 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