proper theory_qualifier;
authorwenzelm
Fri, 21 Apr 2017 10:59:07 +0200
changeset 65528 d15d302da7f0
parent 65527 0d8a7013bf36
child 65529 53fd6cf53ec2
proper theory_qualifier;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 20 17:50:31 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 10:59:07 2017 +0200
@@ -164,7 +164,7 @@
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
                   thys.map({ case (thy, pos) =>
-                    (resources.import_name(info.name, info.dir.implode, thy), pos) })
+                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -210,10 +210,10 @@
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
-                val session = resources.theory_qualifier(name)
-                if (session == info.name)
+                val qualifier = resources.theory_qualifier(name)
+                if (qualifier == info.theory_qualifier)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
-                else session_node(session)
+                else session_node(qualifier)
               }
 
               val imports_subgraph =