--- a/src/Pure/PIDE/resources.ML Sat Apr 08 21:09:34 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Sat Apr 08 21:28:19 2017 +0200
@@ -19,6 +19,7 @@
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val thy_path: Path.T -> Path.T
+ val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
val check_thy: Path.T -> string ->
{master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -98,6 +99,21 @@
val thy_path = Path.ext "thy";
+fun import_name dir path =
+ let
+ val theory0 = Path.implode (Path.base path);
+ val theory =
+ if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
+ else Long_Name.qualify (default_qualifier ()) theory0;
+ val node_name =
+ the (get_first (fn e => e ())
+ [fn () => loaded_theory theory,
+ fn () => loaded_theory theory0,
+ fn () => known_theory theory,
+ fn () => known_theory theory0,
+ fn () => SOME (File.full_path dir (thy_path path))])
+ in {node_name = node_name, theory_name = theory} end;
+
fun check_file dir file = File.check_file (File.full_path dir file);
fun check_thy dir thy_name =