# HG changeset patch
# User wenzelm
# Date 1491592008 -7200
# Node ID a260181505c1db3936874c11f16160f530f72d50
# Parent  d938705819bb7cc07c51f54024639f8c02eec264
refer to known_theory;
support for qualified theory name;

diff -r d938705819bb -r a260181505c1 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Apr 07 20:25:01 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Apr 07 21:06:48 2017 +0200
@@ -82,15 +82,20 @@
 
 fun check_thy dir thy_name =
   let
-    val path = thy_path (Path.basic thy_name);
-    val master_file = check_file dir path;
+    val thy_base_name = Long_Name.base_name thy_name;
+    val thy_path = thy_path (Path.basic thy_base_name);
+    val master_file =
+      (case known_theory thy_name of
+        NONE => check_file dir thy_path
+      | SOME known_path => check_file Path.current known_path);
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
-    val _ = thy_name <> name andalso
-      error ("Bad theory name " ^ quote name ^
-        " for file " ^ Path.print path ^ Position.here pos);
+    val _ =
+      thy_base_name <> name andalso
+        error ("Bad theory name " ^ quote name ^
+          " for file " ^ Path.print thy_path ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}