tuned signature;
authorwenzelm
Tue Sep 04 14:47:50 2018 +0200 (9 months ago)
changeset 6890409151c54aaac
parent 68903 58525b08eed1
child 68905 90a6b714aca3
tuned signature;
src/Pure/PIDE/document_status.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Tue Sep 04 14:40:31 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Tue Sep 04 14:47:50 2018 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4      def apply(name: Document.Node.Name): Node_Status = rep(name)
     1.5      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
     1.6  
     1.7 -    def dest: List[(Document.Node.Name, Node_Status)] =
     1.8 +    def present: List[(Document.Node.Name, Node_Status)] =
     1.9        for { name <- nodes.topological_order; node_status <- get(name) }
    1.10          yield (name, node_status)
    1.11  
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:40:31 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:47:50 2018 +0200
     2.3 @@ -184,7 +184,7 @@
     2.4  
     2.5                      val progress_percentage =
     2.6                        for {
     2.7 -                        (name, node_status) <- nodes_status1.dest.iterator
     2.8 +                        (name, node_status) <- nodes_status1.present.iterator
     2.9                          if changed.nodes.contains(name)
    2.10                          p1 = node_status.percentage
    2.11                          if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
     3.1 --- a/src/Pure/Tools/server.scala	Tue Sep 04 14:40:31 2018 +0200
     3.2 +++ b/src/Pure/Tools/server.scala	Tue Sep 04 14:47:50 2018 +0200
     3.3 @@ -276,7 +276,7 @@
     3.4      override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     3.5      {
     3.6        val json =
     3.7 -        for ((name, node_status) <- nodes_status.dest)
     3.8 +        for ((name, node_status) <- nodes_status.present)
     3.9            yield name.json + ("status" -> nodes_status(name).json)
    3.10        context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
    3.11      }
     4.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Sep 04 14:40:31 2018 +0200
     4.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Sep 04 14:47:50 2018 +0200
     4.3 @@ -222,7 +222,7 @@
     4.4          session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
     4.5  
     4.6      nodes_status = nodes_status1
     4.7 -    if (nodes_status_changed) status.listData = nodes_status1.dest.map(_._1)
     4.8 +    if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)
     4.9    }
    4.10  
    4.11