# HG changeset patch
# User wenzelm
# Date 1514460971 -3600
# Node ID 7ef1c5dada12ecca3e5f81a4df6c03a5ef87ef74
# Parent  417e081322ae751037701bf8b16148e6935e5276
clarified signature;

diff -r 417e081322ae -r 7ef1c5dada12 src/Pure/PIDE/resources.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 */
 
diff -r 417e081322ae -r 7ef1c5dada12 src/Tools/jEdit/src/theories_dockable.scala
--- 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)