# HG changeset patch
# User wenzelm
# Date 1491216066 -7200
# Node ID 403eabd73c9a8326182f2e10f0ec84893e288626
# Parent  d27f9b4e027d7cd22f1b6e1f47c5a4f1e6eb8f91
tuned signature;

diff -r d27f9b4e027d -r 403eabd73c9a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -503,7 +503,7 @@
           case None =>
             List(
               Document.Node.Deps(
-                if (session.resources.base.loaded_theories(node_name.theory))
+                if (session.resources.base.loaded_theory(node_name))
                   node_header.error("Cannot update finished theory " + quote(node_name.theory))
                 else node_header),
               Document.Node.Edits(text_edits), perspective)
diff -r d27f9b4e027d -r 403eabd73c9a src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -88,7 +88,7 @@
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
-      case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
+      case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
       case Some(name) => name
       case None =>
         val path = Path.explode(s)
@@ -155,7 +155,7 @@
   def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     (for {
       (node_name, node) <- nodes.iterator
-      if !base.loaded_theories(node_name.theory)
+      if !base.loaded_theory(node_name)
       cmd <- node.load_commands.iterator
       name <- cmd.blobs_undefined.iterator
     } yield name).toList
diff -r d27f9b4e027d -r 403eabd73c9a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -47,6 +47,10 @@
     syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+  {
+    def loaded_theory(name: Document.Node.Name): Boolean =
+      loaded_theories.contains(name.theory)
+  }
 
   sealed case class Deps(deps: Map[String, Base])
   {
diff -r d27f9b4e027d -r 403eabd73c9a src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -118,7 +118,7 @@
         required_by(initiators) + Position.here(require_pos)
 
     val required1 = required + thy
-    if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
+    if (required.seen(name) || resources.base.loaded_theory(name)) required1
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
diff -r d27f9b4e027d -r 403eabd73c9a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -300,7 +300,7 @@
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     def can_import(name: Document.Node.Name): Boolean =
-      resources.base.loaded_theories(name.theory) || nodes0(name).has_header
+      resources.base.loaded_theory(name) || nodes0(name).has_header
 
     val (doc_edits, version) =
       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
diff -r d27f9b4e027d -r 403eabd73c9a src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -192,7 +192,7 @@
       }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
+          if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty)
             status
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
diff -r d27f9b4e027d -r 403eabd73c9a src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Sat Apr 01 23:48:28 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 12:41:06 2017 +0200
@@ -187,7 +187,7 @@
       }
     val nodes_timing1 =
       (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
-          if (PIDE.resources.base.loaded_theories(name.theory)) timing1
+          if (PIDE.resources.base.loaded_theory(name)) timing1
           else {
             val node_timing =
               Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)