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