optional notification of nodes_status (via progress);
more accurate changed.nodes wrt. dep_theories;
tuned signature;
--- a/NEWS Sat Aug 18 17:29:49 2018 +0200
+++ b/NEWS Sat Aug 18 22:09:09 2018 +0200
@@ -7,6 +7,11 @@
New in this Isabelle version
----------------------------
+*** System ***
+
+* Isabelle server command "use_theories" supports "nodes_status_delay"
+for continuous output of node status information. The time interval is
+specified in seconds; a negative value means it is disabled (default).
New in Isabelle2018 (August 2018)
--- a/src/Doc/System/Server.thy Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Doc/System/Server.thy Sat Aug 18 22:09:09 2018 +0200
@@ -896,7 +896,8 @@
\quad~~\<open>unicode_symbols?: bool,\<close> \\
\quad~~\<open>export_pattern?: string,\<close> \\
\quad~~\<open>check_delay?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
- \quad~~\<open>check_limit?: int}\<close> \\
+ \quad~~\<open>check_limit?: int,\<close> \\
+ \quad~~\<open>nodes_status_delay?: double}\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
\end{tabular}
\begin{tabular}{ll}
@@ -904,6 +905,8 @@
\quad~~\<open>{name: string, base64: bool, body: string}\<close> \\
\<^bold>\<open>type\<close> \<open>node_results =\<close> \\
\quad~~\<open>{status: node_status, messages: [message], exports: [export]}\<close> \\
+ \<^bold>\<open>type\<close> \<open>nodes_status =\<close> \\
+ \quad~~\<open>[node \<oplus> {status: node_status}]\<close> \\
\<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
\quad\<open>{ok: bool,\<close> \\
\quad~~\<open>errors: [message],\<close> \\
@@ -940,6 +943,11 @@
\<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
option @{system_option editor_consolidate_delay} to give PIDE processing a
chance to consolidate document nodes in the first place.
+
+ \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
+ kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
+ interval is specified in seconds; by default it is negative and thus
+ disabled.
\<close>
--- a/src/Pure/PIDE/document_status.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sat Aug 18 22:09:09 2018 +0200
@@ -168,10 +168,15 @@
object Nodes_Status
{
val empty: Nodes_Status = new Nodes_Status(Map.empty)
+
+ type Update = (Nodes_Status, List[Document.Node.Name])
+ val empty_update: Update = (empty, Nil)
}
final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
{
+ def is_empty: Boolean = rep.isEmpty
+ def apply(name: Document.Node.Name): Node_Status = rep(name)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
@@ -186,7 +191,7 @@
state: Document.State,
version: Document.Version,
domain: Option[Set[Document.Node.Name]] = None,
- trim: Boolean = false): Option[(Nodes_Status, List[Document.Node.Name])] =
+ trim: Boolean = false): Option[Nodes_Status.Update] =
{
val nodes = version.nodes
val update_iterator =
--- a/src/Pure/PIDE/markup.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/PIDE/markup.scala Sat Aug 18 22:09:09 2018 +0200
@@ -456,6 +456,7 @@
val WARNING = "warning"
val LEGACY = "legacy"
val ERROR = "error"
+ val NODES_STATUS = "nodes_status"
val PROTOCOL = "protocol"
val SYSTEM = "system"
val STDOUT = "stdout"
--- a/src/Pure/System/progress.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/System/progress.scala Sat Aug 18 22:09:09 2018 +0200
@@ -21,6 +21,7 @@
def echo(msg: String) {}
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
def theory(session: String, theory: String) {}
+ def nodes_status(nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)]) {}
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
--- a/src/Pure/Thy/thy_resources.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Sat Aug 18 22:09:09 2018 +0200
@@ -71,7 +71,8 @@
}
}
- val default_use_theories_check_delay: Double = 0.5
+ val default_check_delay: Double = 0.5
+ val default_nodes_status_delay: Double = -1.0
class Session private[Thy_Resources](
@@ -99,14 +100,16 @@
theories: List[String],
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
- check_delay: Time = Time.seconds(default_use_theories_check_delay),
+ check_delay: Time = Time.seconds(default_check_delay),
check_limit: Int = 0,
+ nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
id: UUID = UUID(),
progress: Progress = No_Progress): Theories_Result =
{
val dep_theories =
resources.load_theories(session, id, theories, qualifier = qualifier,
master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
+ val dep_theories_set = dep_theories.toSet
val result = Future.promise[Theories_Result]
@@ -141,24 +144,51 @@
val theories_progress = Synchronized(Set.empty[Document.Node.Name])
+ val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
+
+ val delay_nodes_status =
+ Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
+ val (nodes_status, names) = nodes_status_update.value
+ progress.nodes_status(names.map(name => (name -> nodes_status(name))))
+ }
+
val consumer =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed =>
- if (dep_theories.exists(changed.nodes)) {
+ if (changed.nodes.exists(dep_theories_set)) {
+ val snapshot = session.snapshot()
+ val state = snapshot.state
+ val version = snapshot.version
+
+ if (nodes_status_delay >= Time.zero) {
+ nodes_status_update.change(
+ { case (nodes_status, names) =>
+ val domain =
+ if (nodes_status.is_empty) dep_theories_set
+ else changed.nodes.iterator.filter(dep_theories_set).toSet
+ val update =
+ nodes_status.update(resources.session_base, state, version,
+ domain = Some(domain), trim = changed.assignment)
+ update match {
+ case None => (nodes_status, names)
+ case Some(upd) => delay_nodes_status.invoke; upd
+ }
+ })
+ }
val check_theories =
- (for (command <- changed.commands.iterator if command.potentially_initialized)
- yield command.node_name).toSet
+ (for {
+ command <- changed.commands.iterator
+ if dep_theories_set(command.node_name) && command.potentially_initialized
+ } yield command.node_name).toSet
if (check_theories.nonEmpty) {
- val snapshot = session.snapshot()
val initialized =
theories_progress.change_result(theories =>
{
val initialized =
(check_theories -- theories).toList.filter(name =>
- Document_Status.Node_Status.make(
- snapshot.state, snapshot.version, name).initialized)
+ Document_Status.Node_Status.make(state, version, name).initialized)
(initialized, theories ++ initialized)
})
initialized.map(_.theory).sorted.foreach(progress.theory("", _))
--- a/src/Pure/Tools/server.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/Tools/server.scala Sat Aug 18 22:09:09 2018 +0200
@@ -268,10 +268,20 @@
override def echo(msg: String): Unit = context.writeln(msg, more:_*)
override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
+
override def theory(session: String, theory: String): Unit =
context.writeln(Progress.theory_message(session, theory),
(List("session" -> session, "theory" -> theory) ::: more.toList):_*)
+ override def nodes_status(
+ nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)])
+ {
+ val json =
+ for ((name, status) <- nodes_status)
+ yield name.json + ("status" -> status.json)
+ context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
+ }
+
@volatile private var is_stopped = false
override def stopped: Boolean = is_stopped
def stop { is_stopped = true }
--- a/src/Pure/Tools/server_commands.scala Sat Aug 18 17:29:49 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala Sat Aug 18 22:09:09 2018 +0200
@@ -158,8 +158,9 @@
pretty_margin: Double = Pretty.default_margin,
unicode_symbols: Boolean = false,
export_pattern: String = "",
- check_delay: Double = Thy_Resources.default_use_theories_check_delay,
- check_limit: Int = 0)
+ check_delay: Double = Thy_Resources.default_check_delay,
+ check_limit: Int = 0,
+ nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
def unapply(json: JSON.T): Option[Args] =
for {
@@ -169,14 +170,16 @@
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
export_pattern <- JSON.string_default(json, "export_pattern")
- check_delay <-
- JSON.double_default(json, "check_delay", Thy_Resources.default_use_theories_check_delay)
+ check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
check_limit <- JSON.int_default(json, "check_limit")
+ nodes_status_delay <-
+ JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
}
yield {
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
unicode_symbols = unicode_symbols, export_pattern = export_pattern,
- check_delay = check_delay, check_limit = check_limit)
+ check_delay = check_delay, check_limit = check_limit,
+ nodes_status_delay = nodes_status_delay)
}
def command(args: Args,
@@ -187,6 +190,7 @@
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
+ nodes_status_delay = Time.seconds(args.nodes_status_delay),
id = id, progress = progress)
def output_text(s: String): String =