# HG changeset patch
# User wenzelm
# Date 1607621906 -3600
# Node ID 626fcaebd049d5deff39eba8ed0ed0db7578be67
# Parent  847c6fb05a215dc97fd9bed2e99515079486dbc5
NEWS and documentation for "isabelle log";

diff -r 847c6fb05a21 -r 626fcaebd049 NEWS
--- a/NEWS	Thu Dec 10 17:41:46 2020 +0100
+++ b/NEWS	Thu Dec 10 18:38:26 2020 +0100
@@ -223,6 +223,9 @@
 
 *** System ***
 
+* The command-line tool "isabelle log" prints messages from the build
+database of the given session.
+
 * Update/rebuild external provers on currently supported OS platforms,
 notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
 
diff -r 847c6fb05a21 -r 626fcaebd049 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Dec 10 17:41:46 2020 +0100
+++ b/src/Doc/System/Sessions.thy	Thu Dec 10 18:38:26 2020 +0100
@@ -509,6 +509,54 @@
 \<close>
 
 
+section \<open>Print messages from build database \label{sec:tool-log}\<close>
+
+text \<open>
+  The @{tool_def "log"} tool prints prover messages from the build
+  database of the given session. Its command-line usage is:
+
+  @{verbatim [display]
+\<open>Usage: isabelle log [OPTIONS] SESSION
+
+  Options are:
+    -T NAME      restrict to given theories (multiple options possible)
+    -U           output Unicode symbols
+    -m MARGIN    margin for pretty printing (default: 76.0)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+
+  Print messages from the build database of the given session, without any
+  checks against current sources: results from a failed build can be
+  printed as well.\<close>}
+
+  The specified session database is taken as is, independently of the current
+  session structure and theories sources. The order of messages follows the
+  source positions of source files; thus the erratic evaluation of parallel
+  processing rarely matters. There is \<^emph>\<open>no\<close> implicit build process involved,
+  so it is possible to retrieve error messages from a failed session as well.
+
+  \<^medskip> Option \<^verbatim>\<open>-o\<close> allows to change system options, as in @{tool build}
+  (\secref{sec:tool-build}). This may affect the storage space for the build
+  database, notably via @{system_option system_heaps}, or @{system_option
+  build_database_server} and its relatives.
+
+  \<^medskip> Option \<^verbatim>\<open>-T\<close> restricts output to given theories: multiple entries are
+  possible by repeating this option on the command-line. The default is to
+  refer to \<^emph>\<open>all\<close> theories that were used in original session build process.
+
+  \<^medskip> Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-U\<close> modify pretty printing and output of Isabelle
+  symbols. The default is for an old-fashioned ASCII terminal at 80 characters
+  per line (76 + 4 characters to prefix warnings or errors).
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+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>}
+\<close>
+
+
 section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
 
 text \<open>
diff -r 847c6fb05a21 -r 626fcaebd049 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Dec 10 17:41:46 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Dec 10 18:38:26 2020 +0100
@@ -162,7 +162,7 @@
 Usage: isabelle log [OPTIONS] SESSION
 
   Options are:
-    -T NAME      restrict to given theories (multiple options)
+    -T NAME      restrict to given theories (multiple options possible)
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: """ + margin + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)