# HG changeset patch
# User wenzelm
# Date 1534622949 -7200
# Node ID add44e2b8cb0514c61e11f84d595c2aed548fbbe
# Parent  59fcff4f8b73b2f2d08ea00d07a15ccc55bbe6c1
optional notification of nodes_status (via progress);
more accurate changed.nodes wrt. dep_theories;
tuned signature;

diff -r 59fcff4f8b73 -r add44e2b8cb0 NEWS
--- 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)
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Doc/System/Server.thy
--- 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>
 
 
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/PIDE/document_status.scala
--- 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 =
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/PIDE/markup.scala
--- 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"
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/System/progress.scala
--- 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)) }
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/Thy/thy_resources.scala
--- 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("", _))
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/Tools/server.scala
--- 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 }
diff -r 59fcff4f8b73 -r add44e2b8cb0 src/Pure/Tools/server_commands.scala
--- 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 =