# HG changeset patch
# User wenzelm
# Date 1567878756 -7200
# Node ID b0172698d0d35abb029c8988685aacf66174d972
# Parent  e4bba654d085aaebca85ce70c220eb360fa072e6
theory_name based on session_directories: no need for expensive all_known;

diff -r e4bba654d085 -r b0172698d0d3 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Sep 07 16:17:30 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Sep 07 19:52:36 2019 +0200
@@ -135,6 +135,16 @@
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
+  def theory_name(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
+  {
+    val dir = File.canonical(file).getParentFile
+    val qualifier = session_base.session_directories.get(dir).map(_._1).getOrElse(default_qualifier)
+    Thy_Header.theory_name(file.getName) match {
+      case "" => None
+      case s => Some(import_name(qualifier, File.path(file).dir.implode, s))
+    }
+  }
+
   def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
     (for {
       (options, thys) <- info.theories.iterator
diff -r e4bba654d085 -r b0172698d0d3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 07 16:17:30 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Sep 07 19:52:36 2019 +0200
@@ -133,8 +133,11 @@
 
   object Base
   {
-    def bootstrap(global_theories: Map[String, String]): Base =
+    def bootstrap(
+        session_directories: Map[JFile, (String, Boolean)],
+        global_theories: Map[String, String]): Base =
       Base(
+        session_directories = session_directories,
         global_theories = global_theories,
         overall_syntax = Thy_Header.bootstrap_syntax)
   }
@@ -142,6 +145,7 @@
   sealed case class Base(
     pos: Position.T = Position.none,
     doc_names: List[String] = Nil,
+    session_directories: Map[JFile, (String, Boolean)] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil,
@@ -183,7 +187,8 @@
       for ((theory, entry) <- known.theories.toList)
         yield (theory, entry.name.node)
 
-    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
+    def get_imports: Base =
+      imports getOrElse Base.bootstrap(session_directories, global_theories)
   }
 
   sealed case class Deps(
@@ -289,7 +294,10 @@
           try {
             val parent_base: Sessions.Base =
               info.parent match {
-                case None => Base.bootstrap(sessions_structure.global_theories)
+                case None =>
+                  Base.bootstrap(
+                    sessions_structure.session_directories,
+                    sessions_structure.global_theories)
                 case Some(parent) => session_bases(parent)
               }
             val imports_base: Sessions.Base =
@@ -386,6 +394,7 @@
               Base(
                 pos = info.pos,
                 doc_names = doc_names,
+                session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = used_theories,