# HG changeset patch
# User wenzelm
# Date 1534594584 -7200
# Node ID 8750edd967cef00afe3562dd03dbd7bf76e97730
# Parent  8bb51b3de39f7540a72d6997069b62b0230298f1
clarified signature;

diff -r 8bb51b3de39f -r 8750edd967ce src/Pure/PIDE/resources.scala
--- 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 */
 
diff -r 8bb51b3de39f -r 8750edd967ce src/Pure/Thy/sessions.scala
--- 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
 
diff -r 8bb51b3de39f -r 8750edd967ce src/Tools/jEdit/src/theories_dockable.scala
--- 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