# HG changeset patch
# User wenzelm
# Date 1514499300 -3600
# Node ID 5f082b1fa9fa8970505a58de71a8a24dcdcafaef
# Parent  2fe338d91d47e71d55baf3eee414be077305b1db
proper check for imports, not just ROOT entries;

diff -r 2fe338d91d47 -r 5f082b1fa9fa src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 28 23:10:30 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 28 23:15:00 2017 +0100
@@ -161,6 +161,8 @@
           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) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)