# HG changeset patch
# User wenzelm
# Date 1595673809 -7200
# Node ID fed7b0ae20d8fe5c6851658f8def93af92d66b6c
# Parent  d3cad9ecd0cce2c150fc3abdf7206cf18e0f1bea
more errors;

diff -r d3cad9ecd0cc -r fed7b0ae20d8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Jul 24 20:43:32 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Jul 25 12:43:29 2020 +0200
@@ -196,10 +196,15 @@
         val header = Thy_Header.read(reader, start, strict)
 
         val base_name = node_name.theory_base_name
-        if (base_name != header.name)
+        if (Long_Name.is_qualified(header.name)) {
+          error("Bad theory name " + quote(header.name) + " with qualification" +
+            Position.here(header.pos))
+        }
+        if (base_name != header.name) {
           error("Bad theory name " + quote(header.name) +
             " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
             Completion.report_theories(header.pos, List(base_name)))
+        }
 
         val imports_pos =
           header.imports_pos.map({ case (s, pos) =>