clarified modules;
authorwenzelm
Sat Aug 18 12:41:05 2018 +0200 (12 months ago ago)
changeset 68758a110e7e24e55
parent 68757 e7e3776385ba
child 68759 4247e91fa21d
clarified modules;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
src/Pure/build-jars
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Aug 17 21:34:56 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Aug 18 12:41:05 2018 +0200
     1.3 @@ -263,9 +263,24 @@
     1.4      def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
     1.5      def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
     1.6  
     1.7 -    lazy val maybe_consolidated: Boolean = Protocol.maybe_consolidated(status)
     1.8 +    lazy val maybe_consolidated: Boolean =
     1.9 +    {
    1.10 +      var touched = false
    1.11 +      var forks = 0
    1.12 +      var runs = 0
    1.13 +      for (markup <- status) {
    1.14 +        markup.name match {
    1.15 +          case Markup.FORKED => touched = true; forks += 1
    1.16 +          case Markup.JOINED => forks -= 1
    1.17 +          case Markup.RUNNING => touched = true; runs += 1
    1.18 +          case Markup.FINISHED => runs -= 1
    1.19 +          case _ =>
    1.20 +        }
    1.21 +      }
    1.22 +      touched && forks == 0 && runs == 0
    1.23 +    }
    1.24  
    1.25 -    lazy val protocol_status: Protocol.Status =
    1.26 +    lazy val document_status: Document_Status.Command_Status =
    1.27      {
    1.28        val warnings =
    1.29          if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
    1.30 @@ -275,7 +290,7 @@
    1.31          if (results.iterator.exists(p => Protocol.is_error(p._2)))
    1.32            List(Markup(Markup.ERROR, Nil))
    1.33          else Nil
    1.34 -      Protocol.Status.make((warnings ::: errors ::: status).iterator)
    1.35 +      Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator)
    1.36      }
    1.37  
    1.38      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.39 @@ -301,7 +316,7 @@
    1.40        status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
    1.41      {
    1.42        val markups1 =
    1.43 -        if (status || Protocol.liberal_status_elements(m.info.name))
    1.44 +        if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
    1.45            markups.add(Markup_Index(true, chunk_name), m)
    1.46          else markups
    1.47        copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 12:41:05 2018 +0200
     2.3 @@ -0,0 +1,159 @@
     2.4 +/*  Title:      Pure/PIDE/document_status.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Document status based on markup information.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Document_Status
    2.14 +{
    2.15 +  /* command status */
    2.16 +
    2.17 +  object Command_Status
    2.18 +  {
    2.19 +    val proper_elements: Markup.Elements =
    2.20 +      Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    2.21 +        Markup.FINISHED, Markup.FAILED)
    2.22 +
    2.23 +    val liberal_elements: Markup.Elements =
    2.24 +      proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    2.25 +
    2.26 +    def make(markup_iterator: Iterator[Markup]): Command_Status =
    2.27 +    {
    2.28 +      var touched = false
    2.29 +      var accepted = false
    2.30 +      var warned = false
    2.31 +      var failed = false
    2.32 +      var forks = 0
    2.33 +      var runs = 0
    2.34 +      for (markup <- markup_iterator) {
    2.35 +        markup.name match {
    2.36 +          case Markup.ACCEPTED => accepted = true
    2.37 +          case Markup.FORKED => touched = true; forks += 1
    2.38 +          case Markup.JOINED => forks -= 1
    2.39 +          case Markup.RUNNING => touched = true; runs += 1
    2.40 +          case Markup.FINISHED => runs -= 1
    2.41 +          case Markup.WARNING | Markup.LEGACY => warned = true
    2.42 +          case Markup.FAILED | Markup.ERROR => failed = true
    2.43 +          case _ =>
    2.44 +        }
    2.45 +      }
    2.46 +      Command_Status(touched, accepted, warned, failed, forks, runs)
    2.47 +    }
    2.48 +
    2.49 +    val empty = make(Iterator.empty)
    2.50 +
    2.51 +    def merge(status_iterator: Iterator[Command_Status]): Command_Status =
    2.52 +      if (status_iterator.hasNext) {
    2.53 +        val status0 = status_iterator.next
    2.54 +        (status0 /: status_iterator)(_ + _)
    2.55 +      }
    2.56 +      else empty
    2.57 +  }
    2.58 +
    2.59 +  sealed case class Command_Status(
    2.60 +    private val touched: Boolean,
    2.61 +    private val accepted: Boolean,
    2.62 +    private val warned: Boolean,
    2.63 +    private val failed: Boolean,
    2.64 +    forks: Int,
    2.65 +    runs: Int)
    2.66 +  {
    2.67 +    def + (that: Command_Status): Command_Status =
    2.68 +      Command_Status(
    2.69 +        touched || that.touched,
    2.70 +        accepted || that.accepted,
    2.71 +        warned || that.warned,
    2.72 +        failed || that.failed,
    2.73 +        forks + that.forks,
    2.74 +        runs + that.runs)
    2.75 +
    2.76 +    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    2.77 +    def is_running: Boolean = runs != 0
    2.78 +    def is_warned: Boolean = warned
    2.79 +    def is_failed: Boolean = failed
    2.80 +    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    2.81 +  }
    2.82 +
    2.83 +
    2.84 +  /* node status */
    2.85 +
    2.86 +  object Node_Status
    2.87 +  {
    2.88 +    def make(
    2.89 +      state: Document.State,
    2.90 +      version: Document.Version,
    2.91 +      name: Document.Node.Name): Node_Status =
    2.92 +    {
    2.93 +      val node = version.nodes(name)
    2.94 +
    2.95 +      var unprocessed = 0
    2.96 +      var running = 0
    2.97 +      var warned = 0
    2.98 +      var failed = 0
    2.99 +      var finished = 0
   2.100 +      for (command <- node.commands.iterator) {
   2.101 +        val states = state.command_states(version, command)
   2.102 +        val status = Command_Status.merge(states.iterator.map(_.document_status))
   2.103 +
   2.104 +        if (status.is_running) running += 1
   2.105 +        else if (status.is_failed) failed += 1
   2.106 +        else if (status.is_warned) warned += 1
   2.107 +        else if (status.is_finished) finished += 1
   2.108 +        else unprocessed += 1
   2.109 +      }
   2.110 +      val initialized = state.node_initialized(version, name)
   2.111 +      val consolidated = state.node_consolidated(version, name)
   2.112 +
   2.113 +      Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
   2.114 +    }
   2.115 +  }
   2.116 +
   2.117 +  sealed case class Node_Status(
   2.118 +    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
   2.119 +    initialized: Boolean, consolidated: Boolean)
   2.120 +  {
   2.121 +    def ok: Boolean = failed == 0
   2.122 +    def total: Int = unprocessed + running + warned + failed + finished
   2.123 +
   2.124 +    def json: JSON.Object.T =
   2.125 +      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   2.126 +        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   2.127 +        "initialized" -> initialized, "consolidated" -> consolidated)
   2.128 +  }
   2.129 +
   2.130 +
   2.131 +  /* node timing */
   2.132 +
   2.133 +  object Node_Timing
   2.134 +  {
   2.135 +    val empty: Node_Timing = Node_Timing(0.0, Map.empty)
   2.136 +
   2.137 +    def make(
   2.138 +      state: Document.State,
   2.139 +      version: Document.Version,
   2.140 +      node: Document.Node,
   2.141 +      threshold: Double): Node_Timing =
   2.142 +    {
   2.143 +      var total = 0.0
   2.144 +      var commands = Map.empty[Command, Double]
   2.145 +      for {
   2.146 +        command <- node.commands.iterator
   2.147 +        st <- state.command_states(version, command)
   2.148 +      } {
   2.149 +        val command_timing =
   2.150 +          (0.0 /: st.status)({
   2.151 +            case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   2.152 +            case (timing, _) => timing
   2.153 +          })
   2.154 +        total += command_timing
   2.155 +        if (command_timing >= threshold) commands += (command -> command_timing)
   2.156 +      }
   2.157 +      Node_Timing(total, commands)
   2.158 +    }
   2.159 +  }
   2.160 +
   2.161 +  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   2.162 +}
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Aug 17 21:34:56 2018 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Aug 18 12:41:05 2018 +0200
     3.3 @@ -38,95 +38,6 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* consolidation status */
     3.8 -
     3.9 -  def maybe_consolidated(markups: List[Markup]): Boolean =
    3.10 -  {
    3.11 -    var touched = false
    3.12 -    var forks = 0
    3.13 -    var runs = 0
    3.14 -    for (markup <- markups) {
    3.15 -      markup.name match {
    3.16 -        case Markup.FORKED => touched = true; forks += 1
    3.17 -        case Markup.JOINED => forks -= 1
    3.18 -        case Markup.RUNNING => touched = true; runs += 1
    3.19 -        case Markup.FINISHED => runs -= 1
    3.20 -        case _ =>
    3.21 -      }
    3.22 -    }
    3.23 -    touched && forks == 0 && runs == 0
    3.24 -  }
    3.25 -
    3.26 -
    3.27 -  /* command status */
    3.28 -
    3.29 -  object Status
    3.30 -  {
    3.31 -    def make(markup_iterator: Iterator[Markup]): Status =
    3.32 -    {
    3.33 -      var touched = false
    3.34 -      var accepted = false
    3.35 -      var warned = false
    3.36 -      var failed = false
    3.37 -      var forks = 0
    3.38 -      var runs = 0
    3.39 -      for (markup <- markup_iterator) {
    3.40 -        markup.name match {
    3.41 -          case Markup.ACCEPTED => accepted = true
    3.42 -          case Markup.FORKED => touched = true; forks += 1
    3.43 -          case Markup.JOINED => forks -= 1
    3.44 -          case Markup.RUNNING => touched = true; runs += 1
    3.45 -          case Markup.FINISHED => runs -= 1
    3.46 -          case Markup.WARNING | Markup.LEGACY => warned = true
    3.47 -          case Markup.FAILED | Markup.ERROR => failed = true
    3.48 -          case _ =>
    3.49 -        }
    3.50 -      }
    3.51 -      Status(touched, accepted, warned, failed, forks, runs)
    3.52 -    }
    3.53 -
    3.54 -    val empty = make(Iterator.empty)
    3.55 -
    3.56 -    def merge(status_iterator: Iterator[Status]): Status =
    3.57 -      if (status_iterator.hasNext) {
    3.58 -        val status0 = status_iterator.next
    3.59 -        (status0 /: status_iterator)(_ + _)
    3.60 -      }
    3.61 -      else empty
    3.62 -  }
    3.63 -
    3.64 -  sealed case class Status(
    3.65 -    private val touched: Boolean,
    3.66 -    private val accepted: Boolean,
    3.67 -    private val warned: Boolean,
    3.68 -    private val failed: Boolean,
    3.69 -    forks: Int,
    3.70 -    runs: Int)
    3.71 -  {
    3.72 -    def + (that: Status): Status =
    3.73 -      Status(
    3.74 -        touched || that.touched,
    3.75 -        accepted || that.accepted,
    3.76 -        warned || that.warned,
    3.77 -        failed || that.failed,
    3.78 -        forks + that.forks,
    3.79 -        runs + that.runs)
    3.80 -
    3.81 -    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    3.82 -    def is_running: Boolean = runs != 0
    3.83 -    def is_warned: Boolean = warned
    3.84 -    def is_failed: Boolean = failed
    3.85 -    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    3.86 -  }
    3.87 -
    3.88 -  val proper_status_elements =
    3.89 -    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    3.90 -      Markup.FINISHED, Markup.FAILED)
    3.91 -
    3.92 -  val liberal_status_elements =
    3.93 -    proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    3.94 -
    3.95 -
    3.96    /* command timing */
    3.97  
    3.98    object Command_Timing
    3.99 @@ -159,80 +70,6 @@
   3.100    }
   3.101  
   3.102  
   3.103 -  /* node status */
   3.104 -
   3.105 -  sealed case class Node_Status(
   3.106 -    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
   3.107 -    initialized: Boolean, consolidated: Boolean)
   3.108 -  {
   3.109 -    def ok: Boolean = failed == 0
   3.110 -    def total: Int = unprocessed + running + warned + failed + finished
   3.111 -
   3.112 -    def json: JSON.Object.T =
   3.113 -      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
   3.114 -        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
   3.115 -        "initialized" -> initialized, "consolidated" -> consolidated)
   3.116 -  }
   3.117 -
   3.118 -  def node_status(
   3.119 -    state: Document.State,
   3.120 -    version: Document.Version,
   3.121 -    name: Document.Node.Name): Node_Status =
   3.122 -  {
   3.123 -    val node = version.nodes(name)
   3.124 -
   3.125 -    var unprocessed = 0
   3.126 -    var running = 0
   3.127 -    var warned = 0
   3.128 -    var failed = 0
   3.129 -    var finished = 0
   3.130 -    for (command <- node.commands.iterator) {
   3.131 -      val states = state.command_states(version, command)
   3.132 -      val status = Status.merge(states.iterator.map(_.protocol_status))
   3.133 -
   3.134 -      if (status.is_running) running += 1
   3.135 -      else if (status.is_failed) failed += 1
   3.136 -      else if (status.is_warned) warned += 1
   3.137 -      else if (status.is_finished) finished += 1
   3.138 -      else unprocessed += 1
   3.139 -    }
   3.140 -    val initialized = state.node_initialized(version, name)
   3.141 -    val consolidated = state.node_consolidated(version, name)
   3.142 -
   3.143 -    Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
   3.144 -  }
   3.145 -
   3.146 -
   3.147 -  /* node timing */
   3.148 -
   3.149 -  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   3.150 -
   3.151 -  val empty_node_timing = Node_Timing(0.0, Map.empty)
   3.152 -
   3.153 -  def node_timing(
   3.154 -    state: Document.State,
   3.155 -    version: Document.Version,
   3.156 -    node: Document.Node,
   3.157 -    threshold: Double): Node_Timing =
   3.158 -  {
   3.159 -    var total = 0.0
   3.160 -    var commands = Map.empty[Command, Double]
   3.161 -    for {
   3.162 -      command <- node.commands.iterator
   3.163 -      st <- state.command_states(version, command)
   3.164 -    } {
   3.165 -      val command_timing =
   3.166 -        (0.0 /: st.status)({
   3.167 -          case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   3.168 -          case (timing, _) => timing
   3.169 -        })
   3.170 -      total += command_timing
   3.171 -      if (command_timing >= threshold) commands += (command -> command_timing)
   3.172 -    }
   3.173 -    Node_Timing(total, commands)
   3.174 -  }
   3.175 -
   3.176 -
   3.177    /* result messages */
   3.178  
   3.179    def is_result(msg: XML.Tree): Boolean =
     4.1 --- a/src/Pure/PIDE/rendering.scala	Fri Aug 17 21:34:56 2018 +0200
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Aug 18 12:41:05 2018 +0200
     4.3 @@ -182,7 +182,7 @@
     4.4        Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
     4.5  
     4.6    val background_elements =
     4.7 -    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
     4.8 +    Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
     4.9        Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    4.10        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    4.11        Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    4.12 @@ -393,7 +393,7 @@
    4.13            command_states =>
    4.14              {
    4.15                case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
    4.16 -              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
    4.17 +              if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
    4.18                  Some((markup :: markups, color))
    4.19                case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
    4.20                  Some((Nil, Some(Rendering.Color.bad)))
    4.21 @@ -431,7 +431,7 @@
    4.22        color <-
    4.23          (result match {
    4.24            case (markups, opt_color) if markups.nonEmpty =>
    4.25 -            val status = Protocol.Status.make(markups.iterator)
    4.26 +            val status = Document_Status.Command_Status.make(markups.iterator)
    4.27              if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
    4.28              else if (status.is_running) Some(Rendering.Color.running1)
    4.29              else opt_color
    4.30 @@ -648,13 +648,14 @@
    4.31      if (snapshot.is_outdated) None
    4.32      else {
    4.33        val results =
    4.34 -        snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
    4.35 -          {
    4.36 -            case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
    4.37 -          }, status = true)
    4.38 +        snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
    4.39 +          _ =>
    4.40 +            {
    4.41 +              case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
    4.42 +            }, status = true)
    4.43        if (results.isEmpty) None
    4.44        else {
    4.45 -        val status = Protocol.Status.make(results.iterator.flatMap(_.info))
    4.46 +        val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
    4.47  
    4.48          if (status.is_running) Some(Rendering.Color.running)
    4.49          else if (status.is_failed) Some(Rendering.Color.error)
     5.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Aug 17 21:34:56 2018 +0200
     5.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Aug 18 12:41:05 2018 +0200
     5.3 @@ -58,7 +58,7 @@
     5.4    class Theories_Result private[Thy_Resources](
     5.5      val state: Document.State,
     5.6      val version: Document.Version,
     5.7 -    val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
     5.8 +    val nodes: List[(Document.Node.Name, Document_Status.Node_Status)])
     5.9    {
    5.10      def node_names: List[Document.Node.Name] = nodes.map(_._1)
    5.11      def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
    5.12 @@ -118,7 +118,7 @@
    5.13              if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) {
    5.14                val nodes =
    5.15                  for (name <- dep_theories)
    5.16 -                yield (name -> Protocol.node_status(state, version, name))
    5.17 +                yield (name -> Document_Status.Node_Status.make(state, version, name))
    5.18                try { result.fulfill(new Theories_Result(state, version, nodes)) }
    5.19                catch { case _: IllegalStateException => }
    5.20              }
    5.21 @@ -157,7 +157,8 @@
    5.22                    {
    5.23                      val initialized =
    5.24                        (check_theories -- theories).toList.filter(name =>
    5.25 -                        Protocol.node_status(snapshot.state, snapshot.version, name).initialized)
    5.26 +                        Document_Status.Node_Status.make(
    5.27 +                          snapshot.state, snapshot.version, name).initialized)
    5.28                      (initialized, theories ++ initialized)
    5.29                    })
    5.30                  initialized.map(_.theory).sorted.foreach(progress.theory("", _))
     6.1 --- a/src/Pure/Tools/dump.scala	Fri Aug 17 21:34:56 2018 +0200
     6.2 +++ b/src/Pure/Tools/dump.scala	Sat Aug 18 12:41:05 2018 +0200
     6.3 @@ -17,7 +17,7 @@
     6.4      deps: Sessions.Deps,
     6.5      output_dir: Path,
     6.6      node_name: Document.Node.Name,
     6.7 -    node_status: Protocol.Node_Status,
     6.8 +    node_status: Document_Status.Node_Status,
     6.9      snapshot: Document.Snapshot)
    6.10    {
    6.11      def write(file_name: Path, bytes: Bytes)
     7.1 --- a/src/Pure/build-jars	Fri Aug 17 21:34:56 2018 +0200
     7.2 +++ b/src/Pure/build-jars	Sat Aug 18 12:41:05 2018 +0200
     7.3 @@ -93,6 +93,7 @@
     7.4    PIDE/command_span.scala
     7.5    PIDE/document.scala
     7.6    PIDE/document_id.scala
     7.7 +  PIDE/document_status.scala
     7.8    PIDE/editor.scala
     7.9    PIDE/line.scala
    7.10    PIDE/markup.scala
     8.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Aug 17 21:34:56 2018 +0200
     8.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 12:41:05 2018 +0200
     8.3 @@ -97,7 +97,7 @@
     8.4  
     8.5    /* component state -- owned by GUI thread */
     8.6  
     8.7 -  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
     8.8 +  private var nodes_status: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty
     8.9    private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
    8.10  
    8.11    private object Overall_Node_Status extends Enumeration
    8.12 @@ -235,7 +235,7 @@
    8.13                  PIDE.resources.session_base.loaded_theory(name) ||
    8.14                  nodes(name).is_empty) status
    8.15              else {
    8.16 -              val st = Protocol.node_status(snapshot.state, snapshot.version, name)
    8.17 +              val st = Document_Status.Node_Status.make(snapshot.state, snapshot.version, name)
    8.18                status + (name -> st)
    8.19              }
    8.20          })
     9.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Aug 17 21:34:56 2018 +0200
     9.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Sat Aug 18 12:41:05 2018 +0200
     9.3 @@ -150,7 +150,7 @@
     9.4  
     9.5    /* component state -- owned by GUI thread */
     9.6  
     9.7 -  private var nodes_timing = Map.empty[Document.Node.Name, Protocol.Node_Timing]
     9.8 +  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
     9.9  
    9.10    private def make_entries(): List[Entry] =
    9.11    {
    9.12 @@ -161,7 +161,7 @@
    9.13          case None => Document.Node.Name.empty
    9.14          case Some(doc_view) => doc_view.model.node_name
    9.15        }
    9.16 -    val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)
    9.17 +    val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
    9.18  
    9.19      val theories =
    9.20        (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
    9.21 @@ -191,7 +191,8 @@
    9.22            if (PIDE.resources.session_base.loaded_theory(name)) timing1
    9.23            else {
    9.24              val node_timing =
    9.25 -              Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)
    9.26 +              Document_Status.Node_Timing.make(
    9.27 +                snapshot.state, snapshot.version, node, timing_threshold)
    9.28              timing1 + (name -> node_timing)
    9.29            }
    9.30        })