# HG changeset patch
# User wenzelm
# Date 1491678574 -7200
# Node ID 1ca6d8a2a00dc5b5d8692aad8e9df85802b39c5a
# Parent  9425e4d8bdb68a5e7f79cee9f56b03b84b897976
clarified;

diff -r 9425e4d8bdb6 -r 1ca6d8a2a00d src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Apr 08 20:56:41 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 21:09:34 2017 +0200
@@ -103,11 +103,10 @@
 fun check_thy dir thy_name =
   let
     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);
+        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;
 
     val {name = (name, pos), imports, keywords} =
@@ -115,7 +114,7 @@
     val _ =
       thy_base_name <> name andalso
         error ("Bad theory name " ^ quote name ^
-          " for file " ^ Path.print thy_path ^ Position.here pos);
+          " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}