# HG changeset patch
# User wenzelm
# Date 1660994175 -7200
# Node ID ccb13acd52833f5c14e14146a53e7edc2a51bbf8
# Parent  16a53676ebbdf9abccd1d2dcab07b56a98569310
tuned;

diff -r 16a53676ebbd -r ccb13acd5283 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Aug 20 12:39:37 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Aug 20 13:16:15 2022 +0200
@@ -232,9 +232,10 @@
         val imports =
           header.imports.map({ case (s, pos) =>
             val name = import_name(node_name, s)
-            if (Sessions.exclude_theory(name.theory_base_name))
+            if (Sessions.exclude_theory(name.theory_base_name)) {
               error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
-            (name, pos)
+            }
+            else (name, pos)
           })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }