# HG changeset patch
# User wenzelm
# Date 1660995947 -7200
# Node ID b327e5d5d6b4a79047233d07146672fd87f1ce18
# Parent  423021c985006ff8c915a15a36f0698ae837c03d
tuned signature;
tuned messages;

diff -r 423021c98500 -r b327e5d5d6b4 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Aug 20 13:35:17 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Aug 20 13:45:47 2022 +0200
@@ -232,8 +232,8 @@
         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))
+            if (Sessions.illegal_theory(name.theory_base_name)) {
+              error("Illegal theory name " + quote(name.theory_base_name) + Position.here(pos))
             }
             else (name, pos)
           })
diff -r 423021c98500 -r b327e5d5d6b4 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 20 13:35:17 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 13:45:47 2022 +0200
@@ -30,8 +30,8 @@
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
-  def exclude_session(name: String): Boolean = name == "" || name == DRAFT
-  def exclude_theory(name: String): Boolean = name == root_name || name == "bib"
+  def illegal_session(name: String): Boolean = name == "" || name == DRAFT
+  def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
 
 
   /* ROOTS file format */
@@ -557,7 +557,7 @@
     try {
       val name = entry.name
 
-      if (exclude_session(name)) error("Bad session name")
+      if (illegal_session(name)) error("Illegal session name " + quote(name))
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
@@ -570,8 +570,9 @@
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts,
             thys.map({ case ((thy, pos), _) =>
-              if (exclude_theory(thy))
-                error("Bad theory name " + quote(thy) + Position.here(pos))
+              if (illegal_theory(thy)) {
+                error("Illegal theory name " + quote(thy) + Position.here(pos))
+              }
               else (thy, pos) })) })
 
       val global_theories =