--- 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;
--- 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;
--- 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;
--- 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 *)
--- 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 =
--- 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 =
--- 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
--- 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";
--- 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 () =
--- 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);
--- 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;