# HG changeset patch
# User wenzelm
# Date 1675087358 -3600
# Node ID 79231a210f5d17bceb6a03f7a1336b93f8505a25
# Parent  5bf9a1b78f932b80afff45567bf90295ff7ec537
observe option "show_states" in headless server (see also 951abf9db857);

diff -r 5bf9a1b78f93 -r 79231a210f5d NEWS
--- a/NEWS	Mon Jan 30 10:15:01 2023 +0100
+++ b/NEWS	Mon Jan 30 15:02:38 2023 +0100
@@ -256,6 +256,11 @@
   > 1 + 1;;
   > #quit;;
 
+* The headless PIDE server (e.g. command-line tool "isabelle server")
+now observes the option "show_states" as given in the server command
+"session_start". If enabled, the server command "use_theories" will
+expose proof state output via its "messages" field.
+
 
 
 New in Isabelle2022 (October 2022)
diff -r 5bf9a1b78f93 -r 79231a210f5d src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Jan 30 10:15:01 2023 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Jan 30 15:02:38 2023 +0100
@@ -67,6 +67,8 @@
     def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout")
     def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay")
 
+    def show_states: Boolean = session_options.bool("show_states")
+
 
     /* temporary directory */
 
diff -r 5bf9a1b78f93 -r 79231a210f5d src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Mon Jan 30 10:15:01 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala	Mon Jan 30 15:02:38 2023 +0100
@@ -244,6 +244,9 @@
         }
       }
 
+      def show_message(tree: XML.Tree): Boolean =
+        Protocol.is_exported(tree) || session.show_states && Protocol.is_state(tree)
+
       val result_json =
         JSON.Object(
           "ok" -> result.ok,
@@ -259,7 +262,7 @@
                 ("status" -> status.json) +
                 ("messages" ->
                   (for {
-                    (tree, pos) <- snapshot.messages if Protocol.is_exported(tree)
+                    (tree, pos) <- snapshot.messages if show_message(tree)
                   } yield output_message(tree, pos))) +
                 ("exports" ->
                   (if (args.export_pattern == "") Nil else {