--- a/NEWS Tue Mar 07 16:23:48 2023 +0100
+++ b/NEWS Tue Mar 07 22:17:47 2023 +0100
@@ -270,6 +270,9 @@
scalable, and supports most options from "isabelle build". Partial
builds are supported as well, e.g. "isabelle update -n -a".
+* The command-line tool "isabelle log" has been renamed to "isabelle
+build_log", to emphasize its relation to "isabelle build".
+
* System option "ML_process_policy" has been renamed to
"process_policy", as it may affect other processes as well (notably in
"isabelle build").
--- a/src/Doc/System/Sessions.thy Tue Mar 07 16:23:48 2023 +0100
+++ b/src/Doc/System/Sessions.thy Tue Mar 07 22:17:47 2023 +0100
@@ -570,7 +570,7 @@
database of the given session. Its command-line usage is:
@{verbatim [display]
-\<open>Usage: isabelle log [OPTIONS] [SESSIONS ...]
+\<open>Usage: isabelle build_log [OPTIONS] [SESSIONS ...]
Options are:
-H REGEX filter messages by matching against head
@@ -628,16 +628,16 @@
text \<open>
Print messages from theory \<^verbatim>\<open>HOL.Nat\<close> of session \<^verbatim>\<open>HOL\<close>, using Unicode
rendering of Isabelle symbols and a margin of 100 characters:
- @{verbatim [display] \<open> isabelle log -T HOL.Nat -U -m 100 HOL\<close>}
+ @{verbatim [display] \<open> isabelle build_log -T HOL.Nat -U -m 100 HOL\<close>}
Print warnings about ambiguous input (inner syntax) of session
\<^verbatim>\<open>HOL-Library\<close>, which is built beforehand:
@{verbatim [display] \<open> isabelle build HOL-Library
- isabelle log -H "Warning" -M "Ambiguous input" HOL-Library\<close>}
+ isabelle build_log -H "Warning" -M "Ambiguous input" HOL-Library\<close>}
Print all errors from all sessions, e.g. from a partial build of
Isabelle/AFP:
- @{verbatim [display] \<open> isabelle log -H "Error" $(isabelle sessions -a -d AFP/thys)\<close>}
+ @{verbatim [display] \<open> isabelle build_log -H "Error" $(isabelle sessions -a -d AFP/thys)\<close>}
\<close>
--- a/src/Pure/Tools/build.scala Tue Mar 07 16:23:48 2023 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 07 22:17:47 2023 +0100
@@ -457,7 +457,7 @@
- /** "isabelle log" **/
+ /** "isabelle build_log" **/
/* theory markup/messages from session database */
@@ -627,7 +627,7 @@
/* command-line wrapper */
- val isabelle_tool3 = Isabelle_Tool("log", "print messages from session build database",
+ val isabelle_tool3 = Isabelle_Tool("build_log", "print messages from session build database",
Scala_Project.here,
{ args =>
/* arguments */
@@ -641,7 +641,7 @@
var verbose = false
val getopts = Getopts("""
-Usage: isabelle log [OPTIONS] [SESSIONS ...]
+Usage: isabelle build_log [OPTIONS] [SESSIONS ...]
Options are:
-H REGEX filter messages by matching against head
--- a/src/Pure/Tools/build_job.scala Tue Mar 07 16:23:48 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Mar 07 22:17:47 2023 +0100
@@ -515,7 +515,7 @@
}
else {
progress.echo(
- session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")")
+ session_name + " FAILED (see also \"isabelle build_log -H Error " + session_name + "\")")
if (!process_result.interrupted) {
val tail = info.options.int("process_output_tail")
val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)