--- a/src/Pure/System/session.ML Wed Jun 17 17:07:26 2009 +0200
+++ b/src/Pure/System/session.ML Wed Jun 17 17:07:26 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 ())