--- a/src/Pure/PIDE/resources.scala Sat Aug 18 13:52:12 2018 +0200
+++ b/src/Pure/PIDE/resources.scala Sat Aug 18 14:16:24 2018 +0200
@@ -194,9 +194,6 @@
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 || name.is_bibtex_theory
-
/* blobs */
--- a/src/Pure/Thy/sessions.scala Sat Aug 18 13:52:12 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Aug 18 14:16:24 2018 +0200
@@ -26,6 +26,9 @@
def is_pure(name: String): Boolean = name == Thy_Header.PURE
+ def is_hidden(name: Document.Node.Name): Boolean =
+ !name.is_theory || name.theory == Sessions.root_name || name.is_bibtex_theory
+
def exclude_session(name: String): Boolean = name == "" || name == DRAFT
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 13:52:12 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 18 14:16:24 2018 +0200
@@ -222,7 +222,7 @@
val nodes_status1 =
(nodes_status /: (restriction.getOrElse(nodes.domain).iterator))(
{ case (status, name) =>
- if (PIDE.resources.is_hidden(name) ||
+ if (Sessions.is_hidden(name) ||
PIDE.resources.session_base.loaded_theory(name) ||
nodes.is_suppressed(name) ||
nodes(name).is_empty) status