# HG changeset patch
# User wenzelm
# Date 1507317240 -7200
# Node ID 925d10a7a610485f0686b49ec54f93f54787c6c5
# Parent  122df1fde073861ce27a5aa9df2d907f214b1793
clarified error for bad session-qualified imports;

diff -r 122df1fde073 -r 925d10a7a610 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Oct 06 17:13:57 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Oct 06 21:14:00 2017 +0200
@@ -123,7 +123,10 @@
       let val node_name =
         (case known_theory theory of
           SOME node_name => node_name
-        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
+        | NONE =>
+            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
+            then Path.explode s
+            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
       in {master_dir = Path.dir node_name, theory_name = theory} end);
 
 fun check_file dir file = File.check_file (File.full_path dir file);
diff -r 122df1fde073 -r 925d10a7a610 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Oct 06 17:13:57 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Oct 06 21:14:00 2017 +0200
@@ -105,10 +105,14 @@
         session_base.known_theory(theory) match {
           case Some(node_name) => node_name
           case None =>
-            val path = Path.explode(s)
-            val node = append(dir, thy_path(path))
-            val master_dir = append(dir, path.dir)
-            Document.Node.Name(node, master_dir, theory)
+            if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
+              Document.Node.Name.loaded_theory(theory)
+            else {
+              val path = Path.explode(s)
+              val node = append(dir, thy_path(path))
+              val master_dir = append(dir, path.dir)
+              Document.Node.Name(node, master_dir, theory)
+            }
         }
     }
 
@@ -136,9 +140,14 @@
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
-    val path = File.check_file(name.path)
-    val reader = Scan.byte_reader(path.file)
-    try { f(reader) } finally { reader.close }
+    val path = name.path
+    if (path.is_file) {
+      val reader = Scan.byte_reader(path.file)
+      try { f(reader) } finally { reader.close }
+    }
+    else if (name.node == name.theory)
+      error("Cannot load theory " + quote(name.theory))
+    else error ("Cannot load theory file " + path)
   }
 
   def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
diff -r 122df1fde073 -r 925d10a7a610 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Oct 06 17:13:57 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Oct 06 21:14:00 2017 +0200
@@ -20,6 +20,7 @@
   val ml_bootstrapN: string
   val ml_roots: string list
   val bootstrap_thys: string list
+  val is_base_name: string -> bool
   val import_name: string -> string
   val args: header parser
   val read: Position.T -> string -> header
@@ -114,6 +115,9 @@
 val ml_roots = ["ML_Root0", "ML_Root"];
 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
 
+fun is_base_name s =
+  s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
+
 val import_name = Path.base_name o Path.explode;