--- a/NEWS Thu Dec 10 22:15:16 2020 +0100
+++ b/NEWS Thu Dec 10 22:44:53 2020 +0100
@@ -223,8 +223,11 @@
*** System ***
-* The command-line tool "isabelle log" prints messages from the build
-database of the given session.
+* The command-line tool "isabelle log" prints prover messages from the
+build database of the given session, following the the order of theory
+sources, instead of erratic parallel evaluation. Consequently, the
+session log file is restricted to system messages of the overall build
+process, and thus becomes more informative.
* 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/Pure/Tools/build_job.scala Thu Dec 10 22:15:16 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Dec 10 22:44:53 2020 +0100
@@ -267,7 +267,6 @@
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
- val messages = new mutable.ListBuffer[XML.Elem]
val command_timings = new mutable.ListBuffer[Properties.T]
val theory_timings = new mutable.ListBuffer[Properties.T]
val session_timings = new mutable.ListBuffer[Properties.T]
@@ -397,9 +396,6 @@
else if (msg.is_stderr) {
stderr ++= Symbol.encode(XML.content(message))
}
- else if (Protocol.is_exported(message)) {
- messages += message
- }
else if (msg.is_exit) {
val err =
"Prover terminated" +
@@ -478,8 +474,6 @@
val more_output =
Library.trim_line(stdout.toString) ::
- messages.toList.map(message =>
- Symbol.encode(Protocol.message_text(message, metric = Symbol.Metric))) :::
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::