clarified terminology of "session build database", while "build database" is the one underlying Build_Process;
--- 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>\<open>$ISABELLE_HOME/browser_info\<close>.
\<^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>\<open>$ISABELLE_HOME_USER/heaps\<close>. If @{system_option system_heaps} is
\<^verbatim>\<open>true\<close>, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default
is \<^path>\<open>$ISABELLE_HOME/heaps\<close>. See also \secref{sec:tool-build}.
--- 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.
\<close>
--- 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 @@
\<close>
-section \<open>Print messages from build database \label{sec:tool-log}\<close>
+section \<open>Print messages from session build database \label{sec:tool-log}\<close>
text \<open>
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
--- 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
--- 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)),
--- 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