--- a/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 17:07:17 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 18:43:44 2009 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:17 2009 +0100
+++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 18:43:44 2009 +0200
@@ -299,8 +299,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
- @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
+ @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+ @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
\end{tabular}
\end{center}
@@ -454,6 +454,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -563,6 +564,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-t"} option produces a more detailed
+ internal timing report of the session.
+
\medskip The @{verbatim "-v"} option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:07:17 2009 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 18:43:44 2009 +0200
@@ -323,8 +323,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
- \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
+ \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
+ \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
\end{tabular}
\end{center}
@@ -480,6 +480,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -580,6 +581,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The \verb|-t| option produces a more detailed
+ internal timing report of the session.
+
\medskip The \verb|-v| option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/lib/Tools/usedir Wed Jun 17 17:07:17 2009 +0100
+++ b/lib/Tools/usedir Wed Jun 17 18:43:44 2009 +0200
@@ -31,6 +31,7 @@
echo " -p LEVEL set level of detail for proof objects"
echo " -r reset session path"
echo " -s NAME override session NAME"
+ echo " -t BOOL internal session timing (default false)"
echo " -v BOOL be verbose (default false)"
echo
echo " Build object-logic or run examples. Also creates browsing"
@@ -84,12 +85,13 @@
RESET=false
SESSION=""
PROOFS=0
+TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -158,6 +160,10 @@
s)
SESSION="$OPTARG"
;;
+ t)
+ check_bool "$OPTARG"
+ TIMING="$OPTARG"
+ ;;
v)
check_bool "$OPTARG"
VERBOSE="$OPTARG"
@@ -229,7 +235,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -238,7 +244,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 18:43:44 2009 +0200
@@ -351,7 +351,7 @@
simps : thm list}
structure DatatypeInterpretation = InterpretationFun
- (type T = datatype_config * string list val eq = eq_snd op =);
+ (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
--- a/src/Pure/General/output.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/General/output.ML Wed Jun 17 18:43:44 2009 +0200
@@ -18,7 +18,6 @@
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
val timing: bool ref
- val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
end;
signature OUTPUT =
@@ -47,7 +46,6 @@
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
- val accumulated_time: unit -> unit
end;
structure Output: OUTPUT =
@@ -141,79 +139,9 @@
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-
(*global timing mode*)
val timing = ref false;
-
-(* accumulated timing *)
-
-local
-
-datatype time_info = TI of
- {name: string,
- timer: Timer.cpu_timer,
- sys: Time.time,
- usr: Time.time,
- gc: Time.time,
- count: int};
-
-fun time_init name = ref (TI
- {name = name,
- timer = Timer.startCPUTimer (),
- sys = Time.zeroTime,
- usr = Time.zeroTime,
- gc = Time.zeroTime,
- count = 0});
-
-fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
-
-fun time_check (ref (TI r)) = r;
-
-fun time_add ti f x =
- let
- fun add_diff time time1 time2 =
- Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
- val {name, timer, sys, usr, gc, count} = time_check ti;
- val (sys1, usr1, gc1) = check_timer timer;
- val result = Exn.capture f x;
- val (sys2, usr2, gc2) = check_timer timer;
- in
- ti := TI
- {name = name,
- timer = timer,
- sys = add_diff sys sys1 sys2,
- usr = add_diff usr usr1 usr2,
- gc = add_diff gc gc1 gc2,
- count = count + 1};
- Exn.release result
- end;
-
-fun time_finish ti =
- let
- fun secs prfx time = prfx ^ Time.toString time;
- val {name, timer, sys, usr, gc, count} = time_check ti;
- in
- warning ("Total of " ^ quote name ^ ": " ^
- secs "User " usr ^ secs " GC " gc ^ secs " All " (Time.+ (sys, Time.+ (usr, gc))) ^
- " secs in " ^ string_of_int count ^ " calls");
- time_reset ti
- end;
-
-val time_finish_hooks = ref ([]: (unit -> unit) list);
-
-in
-
-fun time_accumulator name =
- let val ti = time_init name in
- CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
- time_add ti
- end;
-
-fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
-
-end;
-
end;
structure BasicOutput: BASIC_OUTPUT = Output;
--- a/src/Pure/IsaMakefile Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/IsaMakefile Wed Jun 17 18:43:44 2009 +0200
@@ -29,7 +29,8 @@
ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
- ML-Systems/time_limit.ML ML-Systems/universal.ML
+ ML-Systems/timing.ML ML-Systems/time_limit.ML \
+ ML-Systems/universal.ML
RAW: $(OUT)/RAW
--- a/src/Pure/ML-Systems/mosml.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Wed Jun 17 18:43:44 2009 +0200
@@ -154,10 +154,6 @@
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
in {message = message, user = user, all = all} end;
-fun check_timer timer =
- let val {sys, usr, gc} = Timer.checkCPUTimer timer
- in (sys, usr, gc) end;
-
(* SML basis library fixes *)
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 18:43:44 2009 +0200
@@ -8,6 +8,7 @@
use "ML-Systems/exn.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
val implode = SML90.implode;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(* prompts *)
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
--- a/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 18:43:44 2009 +0200
@@ -12,6 +12,7 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
@@ -59,30 +60,6 @@
end;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(*prompts*)
fun ml_prompts p1 p2 =
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/timing.ML Wed Jun 17 18:43:44 2009 +0200
@@ -0,0 +1,32 @@
+(* Title: Pure/ML-Systems/timing.ML
+ Author: Makarius
+
+Compiler-independent timing functions.
+*)
+
+fun start_timing () =
+ let
+ val real_timer = Timer.startRealTimer ();
+ val real_time = Timer.checkRealTimer real_timer;
+ val cpu_timer = Timer.startCPUTimer ();
+ val cpu_times = Timer.checkCPUTimes cpu_timer;
+ in (real_timer, real_time, cpu_timer, cpu_times) end;
+
+fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
+ let
+ val real_time2 = Timer.checkRealTimer real_timer;
+ val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
+ val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
+ Timer.checkCPUTimes cpu_timer;
+
+ open Time;
+ val elapsed = real_time2 - real_time;
+ val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
+ val cpu = usr2 - usr + sys2 - sys + gc;
+ val gc_percent = Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * toReal gc / toReal cpu);
+ val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+ val message =
+ (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
+ gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
+ in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+
--- a/src/Pure/System/session.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/System/session.ML Wed Jun 17 18:43:44 2009 +0200
@@ -9,8 +9,9 @@
val id: unit -> string list
val name: unit -> string
val welcome: unit -> string
- val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
- string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
+ val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+ string -> bool -> string list -> string -> string -> bool * string ->
+ string -> int -> bool -> bool -> int -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -72,8 +73,7 @@
(* finish *)
fun finish () =
- (Output.accumulated_time ();
- ThyInfo.finish ();
+ (ThyInfo.finish ();
Present.finish ();
Future.shutdown ();
session_finished := true);
@@ -92,13 +92,20 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
-fun use_dir root build modes reset info doc doc_graph doc_versions
- parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
+fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+ name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
(dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
- use root;
+ if timing then
+ let
+ val start = start_timing ();
+ val _ = use root;
+ val stop = end_timing start;
+ val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+ in () end
+ else use root;
finish ()))
|> setmp_noncritical Proofterm.proofs level
|> setmp_noncritical print_mode (modes @ print_mode_value ())
--- a/src/Pure/Tools/find_consts.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML Wed Jun 17 18:43:44 2009 +0200
@@ -25,10 +25,9 @@
| Loose of string
| Name of string;
+
(* matching types/consts *)
-fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
-
fun matches_subtype thy typat =
let
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
@@ -51,7 +50,9 @@
fun filter_const _ NONE = NONE
| filter_const f (SOME (c, r)) =
- Option.map (pair c o (curry Int.min r)) (f c);
+ (case f c of
+ NONE => NONE
+ | SOME i => SOME (c, Int.min (r, i)));
(* pretty results *)
@@ -76,6 +77,7 @@
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
+
(* find_consts *)
fun find_consts ctxt raw_criteria =
@@ -85,16 +87,17 @@
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
- fun not_internal consts (nm, _) =
+ fun not_internal consts (nm, _) =
if member (op =) (Consts.the_tags consts nm) Markup.property_internal
then NONE else SOME low_ranking;
fun make_pattern crit =
let
val raw_T = Syntax.parse_typ ctxt crit;
- val t = Syntax.check_term
- (ProofContext.set_mode ProofContext.mode_pattern ctxt)
- (Term.dummy_pattern raw_T);
+ val t =
+ Syntax.check_term
+ (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+ (Term.dummy_pattern raw_T);
in Term.type_of t end;
fun make_match (Strict arg) =
@@ -102,34 +105,34 @@
fn (_, (ty, _)) =>
let
val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
- val sub_size = Vartab.fold add_tye tye 0;
+ val sub_size =
+ Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
in SOME sub_size end handle MATCH => NONE
end
-
| make_match (Loose arg) =
check_const (matches_subtype thy (make_pattern arg) o snd)
-
| make_match (Name arg) = check_const (match_string arg o fst);
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
val criteria = map make_criterion raw_criteria;
val consts = Sign.consts_of thy;
- val (_, consts_tab) = (#constants o Consts.dest) consts;
- fun eval_entry c = fold filter_const (not_internal consts::criteria)
- (SOME (c, low_ranking));
+ val (_, consts_tab) = #constants (Consts.dest consts);
+ fun eval_entry c =
+ fold filter_const (not_internal consts :: criteria)
+ (SOME (c, low_ranking));
val matches =
Symtab.fold (cons o eval_entry) consts_tab []
|> map_filter I
|> sort (rev_order o int_ord o pairself snd)
- |> map ((apsnd fst) o fst);
+ |> map (apsnd fst o fst);
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
:: Pretty.str ""
- :: (Pretty.str o concat)
+ :: (Pretty.str o implode)
(if null matches
then ["nothing found", end_msg]
else ["found ", (string_of_int o length) matches,
--- a/src/Pure/Tools/find_theorems.ML Wed Jun 17 17:07:17 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Jun 17 18:43:44 2009 +0200
@@ -282,7 +282,7 @@
in app (opt_add r r', consts', fs) end;
in app end;
-
+
in
fun filter_criterion ctxt opt_goal (b, c) =
@@ -417,7 +417,7 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
val returned = length thms;
-
+
val tally_msg =
(case foundo of
NONE => "displaying " ^ string_of_int returned ^ " theorems"
@@ -427,7 +427,7 @@
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
:: Pretty.str "" ::