# HG changeset patch
# User wenzelm
# Date 1514500742 -3600
# Node ID 888aa91f05567b96701758e683e895a96f3a4fc3
# Parent  9b3eb67ab579cd55796a73a0f296021729d2ce19
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);

diff -r 9b3eb67ab579 -r 888aa91f0556 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 28 23:17:35 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 28 23:39:02 2017 +0100
@@ -161,10 +161,14 @@
           error("Bad theory name " + quote(name) +
             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
             Completion.report_theories(pos, List(base_name)))
-        if (Sessions.exclude_theory(name))
-          error("Bad theory name " + quote(name) + Position.here(pos))
 
-        val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
+        val imports =
+          header.imports.map({ case (s, pos) =>
+            val name = import_name(node_name, s)
+            if (Sessions.exclude_theory(name.theory_base_name))
+              error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
+            (name, pos)
+          })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }