# HG changeset patch
# User wenzelm
# Date 1365021065 -7200
# Node ID 0f26c787a7a4c6eda5ddfcabda9f9bc7224527fb
# Parent  197e25f13f0c07eada7bcf5b823c721f67eb1c77# Parent  9c01df6a98434b2472f2c2a8ead6276ad2d9e6e5
merged

diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/General/timing.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -23,6 +23,7 @@
   val is_relevant_time: Time.time -> bool
   val is_relevant: timing -> bool
   val message: timing -> string
+  val status: ('a -> 'b) -> 'a -> 'b
 end
 
 structure Timing: TIMING =
@@ -89,10 +90,10 @@
 fun cond_timeit enabled msg e =
   if enabled then
     let
-      val (timing, result) = timing (Exn.interruptible_capture e) ();
+      val (t, result) = timing (Exn.interruptible_capture e) ();
       val _ =
-        if is_relevant timing then
-          let val end_msg = message timing
+        if is_relevant t then
+          let val end_msg = message t
           in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
         else ();
     in Exn.release result end
@@ -102,6 +103,12 @@
 fun timeap f x = timeit (fn () => f x);
 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
 
+fun status f x =
+  let
+    val (t, result) = timing (Exn.interruptible_capture f) x;
+    val _ = if is_relevant t then Output.status (Markup.markup_only (Markup.timing t)) else ();
+  in Exn.release result end;
+
 end;
 
 structure Basic_Timing: BASIC_TIMING = Timing;
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -1158,24 +1158,23 @@
 
 local
 
-fun future_terminal_proof n proof1 proof2 done int state =
-  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
-    andalso not (is_relevant state)
-  then
+fun future_terminal_proof proof1 proof2 done int state =
+  if Goal.future_enabled_level 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
-      Goal.fork_name "Proof.future_terminal_proof" ~1
-        (fn () => ((), proof2 state'))) |> snd |> done
+      Goal.fork_params
+        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
+        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
   else proof1 state;
 
 in
 
 fun local_future_terminal_proof meths =
-  future_terminal_proof 3
+  future_terminal_proof
     (local_terminal_proof meths)
     (local_terminal_proof meths #> context_of) local_done_proof;
 
 fun global_future_terminal_proof meths =
-  future_terminal_proof 3
+  future_terminal_proof
     (global_terminal_proof meths)
     (global_terminal_proof meths) global_done_proof;
 
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -1317,7 +1317,7 @@
       val prt_prems =
         (case Assumption.all_prems_of ctxt of
           [] => []
-        | prems => [Pretty.big_list "prems:" (map (Display.pretty_thm_item ctxt) prems)]);
+        | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
     in prt_structs @ prt_fixes @ prt_prems end;
 
 
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -113,9 +113,9 @@
 
 fun pretty_goal_facts ctxt s ths =
   (Pretty.block o Pretty.fbreaks)
-    ((if s = "" then Pretty.str "this:"
-      else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
-      map (Display.pretty_thm_item ctxt) ths);
+    [if s = "" then Pretty.str "this:"
+     else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"],
+     Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* method_error *)
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -763,9 +763,10 @@
   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 (timing_estimate true (Thy_Syntax.atom tr)))
-            (fn () => command tr st); st)) ()
+        (Goal.fork_params
+          {name = "Toplevel.diag", pos = pos_of tr,
+            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
+          (fn () => command tr st); st)
       else command tr st;
   in (Result (tr, st'), st') end;
 
@@ -788,19 +789,18 @@
           let
             val finish = Context.Theory o Proof_Context.theory_of;
 
-            val future_proof = Proof.future_proof
-              (fn state =>
-                setmp_thread_position head_tr (fn () =>
-                  Goal.fork_name "Toplevel.future_proof"
-                    (priority estimate)
-                    (fn () =>
-                      let
-                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
-                        val prf' = Proof_Node.apply (K state) prf;
-                        val (result, result_state) =
-                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
-                          |> fold_map element_result body_elems ||> command end_tr;
-                      in (Result_List result, presentation_context_of result_state) end)) ())
+            val future_proof =
+              Proof.future_proof (fn state =>
+                Goal.fork_params
+                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
+                  (fn () =>
+                    let
+                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
+                      val prf' = Proof_Node.apply (K state) prf;
+                      val (result, result_state) =
+                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
+                        |> fold_map element_result body_elems ||> command end_tr;
+                    in (Result_List result, presentation_context_of result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 
             val forked_proof =
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -63,8 +63,8 @@
 
 fun run int tr st =
   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
-    (Goal.fork_name "Toplevel.diag" ~1 (fn () => Toplevel.command_exception int tr st);
-      ([], SOME st))
+    (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
+      (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
 fun check_cmts tr cmts st =
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -94,14 +94,14 @@
   val cpuN: string
   val gcN: string
   val timing_propertiesN: string list
-  val timing_properties: Timing.timing -> Properties.T
-  val parse_timing_properties: Properties.T -> Timing.timing
+  val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
+  val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time}
   val command_timingN: string
   val command_timing_properties:
     {file: string, offset: int, name: string} -> Time.time -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
-  val timingN: string val timing: Timing.timing -> T
+  val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -28,9 +28,9 @@
 
 use "General/properties.ML";
 use "General/output.ML";
-use "General/timing.ML";
 use "PIDE/markup.ML";
 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
+use "General/timing.ML";
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/goal.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -26,7 +26,7 @@
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
@@ -95,10 +95,10 @@
    C
 *)
 fun check_finished ctxt th =
-  (case Thm.nprems_of th of
-    0 => th
-  | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
+  if Thm.no_prems th then th
+  else
+    raise THM ("Proof failed.\n" ^
+      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
@@ -143,10 +143,9 @@
 
 in
 
-fun fork_name name pri e =
-  uninterruptible (fn _ => fn () =>
+fun fork_params {name, pos, pri} e =
+  uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
     let
-      val pos = Position.thread_data ();
       val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
 
@@ -174,9 +173,10 @@
             in Exn.release result end);
       val _ = status (Future.task_of future) [Markup.forked];
       val _ = register_forked id future;
-    in future end) ();
+    in future end)) ();
 
-fun fork pri e = fork_name "Goal.fork" pri e;
+fun fork pri e =
+  fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);
 
@@ -184,7 +184,7 @@
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
 
 fun reset_futures () =
-  Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
+  Synchronized.change_result forked_proofs (fn (_, groups, _) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
 fun shutdown_futures () =
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/tactic.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -157,9 +157,7 @@
 fun distinct_tac (i, k) =
   permute_tac 0 (i - 1) THEN
   permute_tac 1 (k - 1) THEN
-  DETERM (PRIMSEQ (fn st =>
-    Thm.compose_no_flatten false (st, 0) 1
-      (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
+  PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN
   permute_tac 1 (1 - k) THEN
   permute_tac 0 (1 - i);
 
diff -r 197e25f13f0c -r 0f26c787a7a4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 03 22:26:04 2013 +0200
+++ b/src/Pure/thm.ML	Wed Apr 03 22:31:05 2013 +0200
@@ -1377,7 +1377,7 @@
   in addprfs asms 1 end;
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
-  Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
+  Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*)
 fun eq_assumption i state =
   let
     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;