clarified protocol for "verbose" messages;

--- a/NEWS	Sun Mar 05 15:34:00 2023 +0100
+++ b/NEWS	Sun Mar 05 16:14:48 2023 +0100
@@ -295,6 +295,11 @@
 "session_start". If enabled, the server command "use_theories" will
 expose proof state output via its "messages" field.
 
+* Isabelle server command "session_build" no longer supports the
+"verbose" flag. Instead, all messages are shown unconditionally, while
+the property {"verbose": bool} indicates whether the result is meant to
+depend on verbose mode.
+
 
 
 New in Isabelle2022 (October 2022)

--- a/src/Doc/System/Server.thy	Sun Mar 05 15:34:00 2023 +0100
+++ b/src/Doc/System/Server.thy	Sun Mar 05 16:14:48 2023 +0100
@@ -719,10 +719,6 @@
   (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
   (\secref{sec:command-use-theories}) to refer to sources from other sessions
   in a robust manner, instead of relying on directory locations.
-
-  \<^medskip>
-  The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
-  similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
 \<close>
 
 

--- a/src/Pure/Tools/server.scala	Sun Mar 05 15:34:00 2023 +0100
+++ b/src/Pure/Tools/server.scala	Sun Mar 05 16:14:48 2023 +0100
@@ -256,14 +256,16 @@
 
   class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
   extends Progress {
-    override def output(message: Progress.Message): Unit =
-      if (do_output(message)) {
-        message.kind match {
-          case Progress.Kind.writeln => context.writeln(message.text, more:_*)
-          case Progress.Kind.warning => context.warning(message.text, more:_*)
-          case Progress.Kind.error_message => context.error_message(message.text, more:_*)
-        }
+    override def verbose: Boolean = true
+
+    override def output(message: Progress.Message): Unit = {
+      val more1 = ("verbose" -> message.verbose.toString) :: more.toList
+      message.kind match {
+        case Progress.Kind.writeln => context.writeln(message.text, more1:_*)
+        case Progress.Kind.warning => context.warning(message.text, more1:_*)
+        case Progress.Kind.error_message => context.error_message(message.text, more1:_*)
       }
+    }
 
     override def theory(theory: Progress.Theory): Unit = {
       val entries: List[JSON.Object.Entry] =

--- a/src/Pure/Tools/server_commands.scala	Sun Mar 05 15:34:00 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala	Sun Mar 05 16:14:48 2023 +0100
@@ -42,8 +42,7 @@
       preferences: String = default_preferences,
       options: List[String] = Nil,
       dirs: List[String] = Nil,
-      include_sessions: List[String] = Nil,
-      verbose: Boolean = false)
+      include_sessions: List[String] = Nil)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -52,11 +51,10 @@
         options <- JSON.strings_default(json, "options")
         dirs <- JSON.strings_default(json, "dirs")
         include_sessions <- JSON.strings_default(json, "include_sessions")
-        verbose <- JSON.bool_default(json, "verbose")
       }
       yield {
         Args(session, preferences = preferences, options = options, dirs = dirs,
-          include_sessions = include_sessions, verbose = verbose)
+          include_sessions = include_sessions)
       }
 
     def command(
@@ -77,7 +75,7 @@
           build_heap = true,
           dirs = dirs,
           infos = session_background.infos,
-          verbose = args.verbose)
+          verbose = progress.verbose)
 
       val sessions_order =
         session_background.sessions_structure.imports_topological_order.zipWithIndex.