# HG changeset patch
# User wenzelm
# Date 1678223867 -3600
# Node ID cbb49fe8e5a20bb63a9fc5c30b81a4789bd62066
# Parent  14f1fa94f0a5a86da3cfa902ec8f34a8443d13b9
renamed "isabelle log" to "isabelle build_log";

diff -r 14f1fa94f0a5 -r cbb49fe8e5a2 NEWS
--- 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").
diff -r 14f1fa94f0a5 -r cbb49fe8e5a2 src/Doc/System/Sessions.thy
--- 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>
 
 
diff -r 14f1fa94f0a5 -r cbb49fe8e5a2 src/Pure/Tools/build.scala
--- 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
diff -r 14f1fa94f0a5 -r cbb49fe8e5a2 src/Pure/Tools/build_job.scala
--- 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)