src/Tools/jEdit/src/theories_dockable.scala
changeset 68766 43a8d0f08600
parent 68764 b523e903d6e4
child 68767 8292cfd7b819
--- 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()