src/Pure/Thy/thy_info.scala
changeset 65429 fcff401fb609
parent 65407 4546272431e9
child 65439 862bfd2b4fd4
--- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 15:53:06 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Apr 07 16:34:14 2017 +0200
@@ -67,7 +67,7 @@
       val import_errors =
         (for {
           (theory, imports) <- seen_theory.iterator_list
-          if !resources.session_base.loaded_theories(theory)
+          if !resources.session_base.loaded_theories.isDefinedAt(theory)
           if imports.length > 1
         } yield {
           "Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -80,11 +80,12 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Set[String] =
+    def loaded_theories: Map[String, Document.Node.Name] =
       (resources.session_base.loaded_theories /: rev_deps) {
         case (loaded, dep) =>
-          loaded + dep.name.theory +
-            Long_Name.base_name(dep.name.theory)  // legacy
+          val name = dep.name.loaded_theory
+          loaded + (name.theory -> name) +
+            (Long_Name.base_name(name.theory) -> name)  // legacy
       }
 
     def loaded_files: List[Path] =