--- 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.
--- 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>
--- 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)