clarified signature;
authorwenzelm
Sat, 18 Aug 2018 14:16:24 +0200
changeset 68762 8750edd967ce
parent 68761 8bb51b3de39f
child 68763 3c5857c6bc5b
clarified signature;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Tools/jEdit/src/theories_dockable.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 */
 
--- 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