src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Sep 12 13:33:09 2019 +0200
@@ -8,7 +8,8 @@
 sig
   val default_qualifier: string
   val init_session_base:
-    {sessions: (string * Properties.T) list,
+    {session_positions: (string * Properties.T) list,
+     session_directories: (string * string) list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list,
@@ -16,7 +17,6 @@
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
-  val known_theory: string -> Path.T option
   val check_session: Proof.context -> string * Position.T -> string
   val check_doc: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
@@ -24,6 +24,7 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
+  val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
@@ -52,7 +53,8 @@
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
-  {sessions = []: (string * entry) list,
+  {session_positions = []: (string * entry) list,
+   session_directories = Symtab.empty: Path.T list Symtab.table,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table,
@@ -61,10 +63,14 @@
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {sessions, docs, global_theories, loaded_theories, known_theories} =
+fun init_session_base
+    {session_positions, session_directories, docs, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {sessions = sort_by #1 (map (apsnd make_entry) sessions),
+      {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+       session_directories =
+         fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
+           session_directories Symtab.empty,
        docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories,
@@ -73,7 +79,8 @@
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {sessions = [],
+      {session_positions = [],
+       session_directories = Symtab.empty,
        docs = [],
        global_theories = global_theories,
        loaded_theories = loaded_theories,
@@ -83,7 +90,6 @@
 
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
-fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 fun check_name which kind markup ctxt (name, pos) =
   let val entries = get_session_base which in
@@ -106,7 +112,7 @@
   Markup.properties
     (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name);
 
-val check_session = check_name #sessions "session" markup_session;
+val check_session = check_name #session_positions "session" markup_session;
 val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name);
 
 
@@ -157,6 +163,20 @@
   then theory
   else Long_Name.qualify qualifier theory;
 
+fun find_theory_file thy_name =
+  (case Symtab.lookup (get_session_base #known_theories) thy_name of
+    NONE =>
+      let
+        val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
+        val session = theory_qualifier thy_name;
+        val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
+      in
+        dirs |> get_first (fn dir =>
+          let val path = Path.append dir thy_file
+          in if File.is_file path then SOME path else NONE end)
+      end
+  | some => some);
+
 fun import_name qualifier dir s =
   let val theory = theory_name qualifier (Thy_Header.import_name s) in
     if loaded_theory theory
@@ -164,7 +184,7 @@
     else
       let
         val node_name =
-          (case known_theory theory of
+          (case find_theory_file theory of
             SOME node_name => node_name
           | NONE =>
               if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
@@ -179,7 +199,7 @@
   let
     val thy_base_name = Long_Name.base_name thy_name;
     val master_file =
-      (case known_theory thy_name of
+      (case find_theory_file thy_name of
         SOME known_path => check_file Path.current known_path
       | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;