--- 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)
})
--- 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 =