optional notification of nodes_status (via progress);
authorwenzelm
Sat Aug 18 22:09:09 2018 +0200 (11 months ago)
changeset 68770add44e2b8cb0
parent 68769 59fcff4f8b73
child 68771 7e1978b9a4d1
optional notification of nodes_status (via progress);
more accurate changed.nodes wrt. dep_theories;
tuned signature;
NEWS
src/Doc/System/Server.thy
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/markup.scala
src/Pure/System/progress.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/NEWS	Sat Aug 18 17:29:49 2018 +0200
     1.2 +++ b/NEWS	Sat Aug 18 22:09:09 2018 +0200
     1.3 @@ -7,6 +7,11 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* Isabelle server command "use_theories" supports "nodes_status_delay"
    1.10 +for continuous output of node status information. The time interval is
    1.11 +specified in seconds; a negative value means it is disabled (default).
    1.12  
    1.13  
    1.14  New in Isabelle2018 (August 2018)
     2.1 --- a/src/Doc/System/Server.thy	Sat Aug 18 17:29:49 2018 +0200
     2.2 +++ b/src/Doc/System/Server.thy	Sat Aug 18 22:09:09 2018 +0200
     2.3 @@ -896,7 +896,8 @@
     2.4    \quad~~\<open>unicode_symbols?: bool,\<close> \\
     2.5    \quad~~\<open>export_pattern?: string,\<close> \\
     2.6    \quad~~\<open>check_delay?: double,\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>0.5\<close> \\
     2.7 -  \quad~~\<open>check_limit?: int}\<close> \\
     2.8 +  \quad~~\<open>check_limit?: int,\<close> \\
     2.9 +  \quad~~\<open>nodes_status_delay?: double}\<close>  & \<^bold>\<open>default:\<close> \<^verbatim>\<open>-1.0\<close> \\
    2.10    \end{tabular}
    2.11  
    2.12    \begin{tabular}{ll}
    2.13 @@ -904,6 +905,8 @@
    2.14    \quad~~\<open>{name: string, base64: bool, body: string}\<close> \\
    2.15    \<^bold>\<open>type\<close> \<open>node_results =\<close> \\
    2.16    \quad~~\<open>{status: node_status, messages: [message], exports: [export]}\<close> \\
    2.17 +  \<^bold>\<open>type\<close> \<open>nodes_status =\<close> \\
    2.18 +  \quad~~\<open>[node \<oplus> {status: node_status}]\<close> \\
    2.19    \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
    2.20    \quad\<open>{ok: bool,\<close> \\
    2.21    \quad~~\<open>errors: [message],\<close> \\
    2.22 @@ -940,6 +943,11 @@
    2.23    \<open>check_delay \<times> check_limit\<close> seconds; it needs to be greater than the system
    2.24    option @{system_option editor_consolidate_delay} to give PIDE processing a
    2.25    chance to consolidate document nodes in the first place.
    2.26 +
    2.27 +  \<^medskip> A non-negative \<open>nodes_status_delay\<close> enables continuous notifications of
    2.28 +  kind \<open>nodes_status\<close>, with a field of name and type \<open>nodes_status\<close>. The time
    2.29 +  interval is specified in seconds; by default it is negative and thus
    2.30 +  disabled.
    2.31  \<close>
    2.32  
    2.33  
     3.1 --- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 17:29:49 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 22:09:09 2018 +0200
     3.3 @@ -168,10 +168,15 @@
     3.4    object Nodes_Status
     3.5    {
     3.6      val empty: Nodes_Status = new Nodes_Status(Map.empty)
     3.7 +
     3.8 +    type Update = (Nodes_Status, List[Document.Node.Name])
     3.9 +    val empty_update: Update = (empty, Nil)
    3.10    }
    3.11  
    3.12    final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status])
    3.13    {
    3.14 +    def is_empty: Boolean = rep.isEmpty
    3.15 +    def apply(name: Document.Node.Name): Node_Status = rep(name)
    3.16      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
    3.17  
    3.18      def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
    3.19 @@ -186,7 +191,7 @@
    3.20        state: Document.State,
    3.21        version: Document.Version,
    3.22        domain: Option[Set[Document.Node.Name]] = None,
    3.23 -      trim: Boolean = false): Option[(Nodes_Status, List[Document.Node.Name])] =
    3.24 +      trim: Boolean = false): Option[Nodes_Status.Update] =
    3.25      {
    3.26        val nodes = version.nodes
    3.27        val update_iterator =
     4.1 --- a/src/Pure/PIDE/markup.scala	Sat Aug 18 17:29:49 2018 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Sat Aug 18 22:09:09 2018 +0200
     4.3 @@ -456,6 +456,7 @@
     4.4    val WARNING = "warning"
     4.5    val LEGACY = "legacy"
     4.6    val ERROR = "error"
     4.7 +  val NODES_STATUS = "nodes_status"
     4.8    val PROTOCOL = "protocol"
     4.9    val SYSTEM = "system"
    4.10    val STDOUT = "stdout"
     5.1 --- a/src/Pure/System/progress.scala	Sat Aug 18 17:29:49 2018 +0200
     5.2 +++ b/src/Pure/System/progress.scala	Sat Aug 18 22:09:09 2018 +0200
     5.3 @@ -21,6 +21,7 @@
     5.4    def echo(msg: String) {}
     5.5    def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
     5.6    def theory(session: String, theory: String) {}
     5.7 +  def nodes_status(nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)]) {}
     5.8  
     5.9    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
    5.10    def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
     6.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Aug 18 17:29:49 2018 +0200
     6.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Aug 18 22:09:09 2018 +0200
     6.3 @@ -71,7 +71,8 @@
     6.4      }
     6.5    }
     6.6  
     6.7 -  val default_use_theories_check_delay: Double = 0.5
     6.8 +  val default_check_delay: Double = 0.5
     6.9 +  val default_nodes_status_delay: Double = -1.0
    6.10  
    6.11  
    6.12    class Session private[Thy_Resources](
    6.13 @@ -99,14 +100,16 @@
    6.14        theories: List[String],
    6.15        qualifier: String = Sessions.DRAFT,
    6.16        master_dir: String = "",
    6.17 -      check_delay: Time = Time.seconds(default_use_theories_check_delay),
    6.18 +      check_delay: Time = Time.seconds(default_check_delay),
    6.19        check_limit: Int = 0,
    6.20 +      nodes_status_delay: Time = Time.seconds(default_nodes_status_delay),
    6.21        id: UUID = UUID(),
    6.22        progress: Progress = No_Progress): Theories_Result =
    6.23      {
    6.24        val dep_theories =
    6.25          resources.load_theories(session, id, theories, qualifier = qualifier,
    6.26            master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
    6.27 +      val dep_theories_set = dep_theories.toSet
    6.28  
    6.29        val result = Future.promise[Theories_Result]
    6.30  
    6.31 @@ -141,24 +144,51 @@
    6.32  
    6.33        val theories_progress = Synchronized(Set.empty[Document.Node.Name])
    6.34  
    6.35 +      val nodes_status_update = Synchronized(Document_Status.Nodes_Status.empty_update)
    6.36 +
    6.37 +      val delay_nodes_status =
    6.38 +        Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
    6.39 +          val (nodes_status, names) = nodes_status_update.value
    6.40 +          progress.nodes_status(names.map(name => (name -> nodes_status(name))))
    6.41 +        }
    6.42 +
    6.43        val consumer =
    6.44          Session.Consumer[Session.Commands_Changed](getClass.getName) {
    6.45            case changed =>
    6.46 -            if (dep_theories.exists(changed.nodes)) {
    6.47 +            if (changed.nodes.exists(dep_theories_set)) {
    6.48 +              val snapshot = session.snapshot()
    6.49 +              val state = snapshot.state
    6.50 +              val version = snapshot.version
    6.51 +
    6.52 +              if (nodes_status_delay >= Time.zero) {
    6.53 +                nodes_status_update.change(
    6.54 +                  { case (nodes_status, names) =>
    6.55 +                      val domain =
    6.56 +                        if (nodes_status.is_empty) dep_theories_set
    6.57 +                        else changed.nodes.iterator.filter(dep_theories_set).toSet
    6.58 +                      val update =
    6.59 +                        nodes_status.update(resources.session_base, state, version,
    6.60 +                          domain = Some(domain), trim = changed.assignment)
    6.61 +                      update match {
    6.62 +                        case None => (nodes_status, names)
    6.63 +                        case Some(upd) => delay_nodes_status.invoke; upd
    6.64 +                      }
    6.65 +                  })
    6.66 +              }
    6.67  
    6.68                val check_theories =
    6.69 -                (for (command <- changed.commands.iterator if command.potentially_initialized)
    6.70 -                  yield command.node_name).toSet
    6.71 +                (for {
    6.72 +                  command <- changed.commands.iterator
    6.73 +                  if dep_theories_set(command.node_name) && command.potentially_initialized
    6.74 +                } yield command.node_name).toSet
    6.75  
    6.76                if (check_theories.nonEmpty) {
    6.77 -                val snapshot = session.snapshot()
    6.78                  val initialized =
    6.79                    theories_progress.change_result(theories =>
    6.80                    {
    6.81                      val initialized =
    6.82                        (check_theories -- theories).toList.filter(name =>
    6.83 -                        Document_Status.Node_Status.make(
    6.84 -                          snapshot.state, snapshot.version, name).initialized)
    6.85 +                        Document_Status.Node_Status.make(state, version, name).initialized)
    6.86                      (initialized, theories ++ initialized)
    6.87                    })
    6.88                  initialized.map(_.theory).sorted.foreach(progress.theory("", _))
     7.1 --- a/src/Pure/Tools/server.scala	Sat Aug 18 17:29:49 2018 +0200
     7.2 +++ b/src/Pure/Tools/server.scala	Sat Aug 18 22:09:09 2018 +0200
     7.3 @@ -268,10 +268,20 @@
     7.4      override def echo(msg: String): Unit = context.writeln(msg, more:_*)
     7.5      override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     7.6      override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
     7.7 +
     7.8      override def theory(session: String, theory: String): Unit =
     7.9        context.writeln(Progress.theory_message(session, theory),
    7.10          (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
    7.11  
    7.12 +    override def nodes_status(
    7.13 +      nodes_status: List[(Document.Node.Name, Document_Status.Node_Status)])
    7.14 +    {
    7.15 +      val json =
    7.16 +        for ((name, status) <- nodes_status)
    7.17 +        yield name.json + ("status" -> status.json)
    7.18 +      context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
    7.19 +    }
    7.20 +
    7.21      @volatile private var is_stopped = false
    7.22      override def stopped: Boolean = is_stopped
    7.23      def stop { is_stopped = true }
     8.1 --- a/src/Pure/Tools/server_commands.scala	Sat Aug 18 17:29:49 2018 +0200
     8.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Aug 18 22:09:09 2018 +0200
     8.3 @@ -158,8 +158,9 @@
     8.4        pretty_margin: Double = Pretty.default_margin,
     8.5        unicode_symbols: Boolean = false,
     8.6        export_pattern: String = "",
     8.7 -      check_delay: Double = Thy_Resources.default_use_theories_check_delay,
     8.8 -      check_limit: Int = 0)
     8.9 +      check_delay: Double = Thy_Resources.default_check_delay,
    8.10 +      check_limit: Int = 0,
    8.11 +      nodes_status_delay: Double = Thy_Resources.default_nodes_status_delay)
    8.12  
    8.13      def unapply(json: JSON.T): Option[Args] =
    8.14        for {
    8.15 @@ -169,14 +170,16 @@
    8.16          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    8.17          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    8.18          export_pattern <- JSON.string_default(json, "export_pattern")
    8.19 -        check_delay <-
    8.20 -          JSON.double_default(json, "check_delay", Thy_Resources.default_use_theories_check_delay)
    8.21 +        check_delay <- JSON.double_default(json, "check_delay", Thy_Resources.default_check_delay)
    8.22          check_limit <- JSON.int_default(json, "check_limit")
    8.23 +        nodes_status_delay <-
    8.24 +          JSON.double_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay)
    8.25        }
    8.26        yield {
    8.27          Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    8.28            unicode_symbols = unicode_symbols, export_pattern = export_pattern,
    8.29 -          check_delay = check_delay, check_limit = check_limit)
    8.30 +          check_delay = check_delay, check_limit = check_limit,
    8.31 +          nodes_status_delay = nodes_status_delay)
    8.32        }
    8.33  
    8.34      def command(args: Args,
    8.35 @@ -187,6 +190,7 @@
    8.36        val result =
    8.37          session.use_theories(args.theories, master_dir = args.master_dir,
    8.38            check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit,
    8.39 +          nodes_status_delay = Time.seconds(args.nodes_status_delay),
    8.40            id = id, progress = progress)
    8.41  
    8.42        def output_text(s: String): String =