--- 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)
--- 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 */
--- 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 {