--- 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;