--- 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)