# HG changeset patch # User wenzelm # Date 1245252274 -7200 # Node ID 57715a08e4b634b8bedab880808fc8932b16a43a # Parent cc37bf07f9bb375cd372b8b50a9b1db2f28972b5# Parent 84a14d2dc86872109eabd19f3fa4ad244eef9e02 merged diff -r cc37bf07f9bb -r 57715a08e4b6 Admin/isatest/settings/at-mac-poly-5.1-para --- a/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 15:41:49 2009 +0200 +++ b/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 17:24:34 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" diff -r cc37bf07f9bb -r 57715a08e4b6 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 15:41:49 2009 +0200 +++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:24:34 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. diff -r cc37bf07f9bb -r 57715a08e4b6 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 15:41:49 2009 +0200 +++ b/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:24:34 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. diff -r cc37bf07f9bb -r 57715a08e4b6 lib/Tools/usedir --- a/lib/Tools/usedir Wed Jun 17 15:41:49 2009 +0200 +++ b/lib/Tools/usedir Wed Jun 17 17:24:34 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 .. diff -r cc37bf07f9bb -r 57715a08e4b6 src/HOL/Tools/datatype_package/datatype_package.ML --- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 17:24:34 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); diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/General/output.ML Wed Jun 17 17:24:34 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; diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/IsaMakefile Wed Jun 17 17:24:34 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 diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/ML-Systems/mosml.ML Wed Jun 17 17:24:34 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 *) diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 17:24:34 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); diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 17:24:34 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); diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/ML-Systems/timing.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/timing.ML Wed Jun 17 17:24:34 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_ratio = Real.fmt (StringCvt.FIX (SOME 2)) (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_ratio ^ "% GC time, factor " ^ factor) handle Time => ""; + in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; + diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/System/session.ML Wed Jun 17 17:24:34 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 ()) diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/Tools/find_consts.ML Wed Jun 17 17:24:34 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, diff -r cc37bf07f9bb -r 57715a08e4b6 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Wed Jun 17 15:41:49 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Jun 17 17:24:34 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 "" ::