# HG changeset patch
# User wenzelm
# Date 1536065270 -7200
# Node ID 09151c54aaac6b40e6fb2a6dce8ad1298a927f5d
# Parent  58525b08eed16bf23afc43a210f3dedb1144eca1
tuned signature;

diff -r 58525b08eed1 -r 09151c54aaac src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Sep 04 14:40:31 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 04 14:47:50 2018 +0200
@@ -230,7 +230,7 @@
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
-    def dest: List[(Document.Node.Name, Node_Status)] =
+    def present: List[(Document.Node.Name, Node_Status)] =
       for { name <- nodes.topological_order; node_status <- get(name) }
         yield (name, node_status)
 
diff -r 58525b08eed1 -r 09151c54aaac src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:40:31 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Tue Sep 04 14:47:50 2018 +0200
@@ -184,7 +184,7 @@
 
                     val progress_percentage =
                       for {
-                        (name, node_status) <- nodes_status1.dest.iterator
+                        (name, node_status) <- nodes_status1.present.iterator
                         if changed.nodes.contains(name)
                         p1 = node_status.percentage
                         if p1 > 0 && Some(p1) != nodes_status.get(name).map(_.percentage)
diff -r 58525b08eed1 -r 09151c54aaac src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Sep 04 14:40:31 2018 +0200
+++ b/src/Pure/Tools/server.scala	Tue Sep 04 14:47:50 2018 +0200
@@ -276,7 +276,7 @@
     override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     {
       val json =
-        for ((name, node_status) <- nodes_status.dest)
+        for ((name, node_status) <- nodes_status.present)
           yield name.json + ("status" -> nodes_status(name).json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
diff -r 58525b08eed1 -r 09151c54aaac src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Sep 04 14:40:31 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Sep 04 14:47:50 2018 +0200
@@ -222,7 +222,7 @@
         session_base, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
-    if (nodes_status_changed) status.listData = nodes_status1.dest.map(_._1)
+    if (nodes_status_changed) status.listData = nodes_status1.present.map(_._1)
   }