# HG changeset patch
# User wenzelm
# Date 1534596953 -7200
# Node ID 43a8d0f08600eb7432223867485cb1dce7d58000
# Parent  be5f255a9943c5aae5cef5460d4694abc62e4461
tuned signature;

diff -r be5f255a9943 -r 43a8d0f08600 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:53:21 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Aug 18 14:55:53 2018 +0200
@@ -185,13 +185,13 @@
       session_base: Sessions.Base,
       state: Document.State,
       version: Document.Version,
-      restriction: Option[Set[Document.Node.Name]],
+      domain: Option[Set[Document.Node.Name]],
       trim: Boolean): Option[(Nodes_Status, List[Document.Node.Name])] =
     {
       val nodes = version.nodes
       val update_iterator =
         for {
-          name <- restriction.getOrElse(nodes.domain).iterator
+          name <- domain.getOrElse(nodes.domain).iterator
           if !Sessions.is_hidden(name) &&
               !session_base.loaded_theory(name) &&
               !nodes.is_suppressed(name) &&
diff -r be5f255a9943 -r 43a8d0f08600 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:53:21 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Aug 18 14:55:53 2018 +0200
@@ -210,9 +210,7 @@
   }
   status.renderer = new Node_Renderer
 
-  private def handle_update(
-    restriction: Option[Set[Document.Node.Name]] = None,
-    trim: Boolean = false)
+  private def handle_update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false)
   {
     GUI_Thread.require {}
 
@@ -221,7 +219,7 @@
     for {
       (nodes_status1, nodes_list) <-
         nodes_status.update(
-          PIDE.resources.session_base, snapshot.state, snapshot.version, restriction, trim)
+          PIDE.resources.session_base, snapshot.state, snapshot.version, domain, trim)
     } {
       nodes_status = nodes_status1
       status.listData = nodes_list
@@ -245,9 +243,7 @@
         }
 
       case changed: Session.Commands_Changed =>
-        GUI_Thread.later {
-          handle_update(restriction = Some(changed.nodes), trim = changed.assignment)
-        }
+        GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
     }
 
   override def init()