# HG changeset patch
# User wenzelm
# Date 1623187439 -7200
# Node ID f72335f6a9edf6c7f5b3a1d29910b6a43f35defa
# Parent  690fdc14f7fba1838e6d09a49ba25cd02948b200
clarified documentation: tracing messages are not shown here;

diff -r 690fdc14f7fb -r f72335f6a9ed src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Jun 08 16:32:57 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Jun 08 23:23:59 2021 +0200
@@ -542,6 +542,7 @@
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: 76.0)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -v           print all messages, including information etc.
 
   Print messages from the build database of the given session, without any
   checks against current sources: results from a failed build can be
@@ -566,8 +567,8 @@
   symbols. The default is for an old-fashioned ASCII terminal at 80 characters
   per line (76 + 4 characters to prefix warnings or errors).
 
-  \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database, including
-  extra information and tracing messages etc.
+  \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are
+  normally inlined into the source text, including information messages etc.
 \<close>
 
 subsubsection \<open>Examples\<close>
diff -r 690fdc14f7fb -r f72335f6a9ed src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Jun 08 16:32:57 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue Jun 08 23:23:59 2021 +0200
@@ -170,7 +170,7 @@
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: """ + margin + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -v           print all messages, including information, tracing etc.
+    -v           print all messages, including information etc.
 
   Print messages from the build database of the given session, without any
   checks against current sources: results from a failed build can be