src/Pure/PIDE/document_status.scala
changeset 69255 800b1ce96fce
parent 68904 09151c54aaac
child 69817 5f160df596c1
--- a/src/Pure/PIDE/document_status.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/PIDE/document_status.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -248,7 +248,7 @@
       }
 
     def update(
-      session_base: Sessions.Base,
+      resources: Resources,
       state: Document.State,
       version: Document.Version,
       domain: Option[Set[Document.Node.Name]] = None,
@@ -258,8 +258,8 @@
       val update_iterator =
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
-          if !Sessions.is_hidden(name) &&
-              !session_base.loaded_theory(name) &&
+          if !resources.is_hidden(name) &&
+              !resources.session_base.loaded_theory(name) &&
               !nodes1.is_suppressed(name) &&
               !nodes1(name).is_empty
           st = Document_Status.Node_Status.make(state, version, name)