--- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 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:26 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:07:26 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:26 2009 +0200
+++ b/lib/Tools/usedir Wed Jun 17 17:07:26 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/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 ())