# HG changeset patch # User wenzelm # Date 1678183070 -3600 # Node ID 4465d9dff4486ce8b0daa247d2bc942138260c4f # Parent 570f65953173848d6bbc1c8f8976fbdf1c1ee3aa clarified terminology of "session build database", while "build database" is the one underlying Build_Process; diff -r 570f65953173 -r 4465d9dff448 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Doc/System/Environment.thy Tue Mar 07 10:57:50 2023 +0100 @@ -168,7 +168,7 @@ used instead; its default is \<^path>\$ISABELLE_HOME/browser_info\. \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images, - log files, and build databases are stored; its default is + log files, and session build databases are stored; its default is \<^path>\$ISABELLE_HOME_USER/heaps\. If @{system_option system_heaps} is \<^verbatim>\true\, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default is \<^path>\$ISABELLE_HOME/heaps\. See also \secref{sec:tool-build}. diff -r 570f65953173 -r 4465d9dff448 src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Doc/System/Presentation.thy Tue Mar 07 10:57:50 2023 +0100 @@ -22,7 +22,7 @@ with the PDF into the given directory (relative to the session directory). Alternatively, @{tool_ref document} may be used to turn the generated - {\LaTeX} sources of a session (exports from its build database) into PDF. + {\LaTeX} sources of a session (exports from its session build database) into PDF. \ diff -r 570f65953173 -r 4465d9dff448 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Doc/System/Sessions.thy Tue Mar 07 10:57:50 2023 +0100 @@ -375,7 +375,7 @@ -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files - -n no build -- take existing build databases + -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants @@ -563,7 +563,7 @@ \ -section \Print messages from build database \label{sec:tool-log}\ +section \Print messages from session build database \label{sec:tool-log}\ text \ The @{tool_def "log"} tool prints prover messages from the build @@ -581,9 +581,9 @@ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v print all messages, including information etc. - Print messages from the build database of the given sessions, without any - checks against current sources nor session structure: results from old - sessions or failed builds can be printed as well. + Print messages from the session build database of the given sessions, + without any checks against current sources nor session structure: results + from old sessions or failed builds can be printed as well. Multiple options -H and -M are conjunctive: all given patterns need to match. Patterns match any substring, but ^ or $ may be used to match the @@ -791,7 +791,7 @@ -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -l NAME additional base logic - -n no build -- take existing build databases + -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u OPT override "update" option for selected sessions -v verbose diff -r 570f65953173 -r 4465d9dff448 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Pure/Tools/build.scala Tue Mar 07 10:57:50 2023 +0100 @@ -258,7 +258,7 @@ -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files - -n no build -- take existing build databases + -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants @@ -535,7 +535,7 @@ /* command-line wrapper */ - val isabelle_tool2 = Isabelle_Tool("log", "print messages from build database", + val isabelle_tool2 = Isabelle_Tool("log", "print messages from session build database", Scala_Project.here, { args => /* arguments */ @@ -560,9 +560,9 @@ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v print all messages, including information etc. - Print messages from the build database of the given sessions, without any - checks against current sources nor session structure: results from old - sessions or failed builds can be printed as well. + Print messages from the session build database of the given sessions, + without any checks against current sources nor session structure: results + from old sessions or failed builds can be printed as well. Multiple options -H and -M are conjunctive: all given patterns need to match. Patterns match any substring, but ^ or $ may be used to match the diff -r 570f65953173 -r 4465d9dff448 src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Pure/Tools/profiling_report.scala Tue Mar 07 10:57:50 2023 +0100 @@ -57,7 +57,7 @@ -c clean function names -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - Report Poly/ML profiling from the build database of the given session + Report Poly/ML profiling from the sebuild database of the given session (without up-to-date check of sources). """, "T:" -> (arg => theories = theories ::: List(arg)), diff -r 570f65953173 -r 4465d9dff448 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Pure/Tools/update.scala Tue Mar 07 10:57:50 2023 +0100 @@ -171,7 +171,7 @@ -j INT maximum number of parallel jobs (default 1) -l NAMES comma-separated list of base logics, to remain unchanged (default: """ + quote(default_base_logic) + """) - -n no build -- take existing build databases + -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u OPT override "update" option for selected sessions -v verbose