clarified signature;
authorwenzelm
Thu, 28 Dec 2017 12:36:11 +0100
changeset 67287 7ef1c5dada12
parent 67286 417e081322ae
child 67288 aa9d28034945
clarified signature;
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 28 12:26:57 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 28 12:36:11 2017 +0100
@@ -188,6 +188,9 @@
     else Some(Document.Node.Header(imports.map((_, Position.none))))
   }
 
+  def is_hidden(name: Document.Node.Name): Boolean =
+    !name.is_theory || name.theory == Sessions.root_name
+
 
   /* blobs */
 
--- a/src/Tools/jEdit/src/theories_dockable.scala	Thu Dec 28 12:26:57 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Thu Dec 28 12:36:11 2017 +0100
@@ -235,9 +235,9 @@
       }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (!name.is_theory ||
-              name.theory == Sessions.root_name ||
-              PIDE.resources.session_base.loaded_theory(name) || node.is_empty) status
+          if (PIDE.resources.is_hidden(name) ||
+              PIDE.resources.session_base.loaded_theory(name) ||
+              node.is_empty) status
           else {
             val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
             status + (name -> st)