more thorough check, without path name artifacts (e.g. "./README");
--- a/src/Pure/Thy/sessions.scala Sat Aug 20 13:45:47 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Aug 20 14:03:40 2022 +0200
@@ -570,8 +570,9 @@
entry.theories.map({ case (opts, thys) =>
(session_options ++ opts,
thys.map({ case ((thy, pos), _) =>
- if (illegal_theory(thy)) {
- error("Illegal theory name " + quote(thy) + Position.here(pos))
+ val thy_name = Thy_Header.import_name(thy)
+ if (illegal_theory(thy_name)) {
+ error("Illegal theory name " + quote(thy_name) + Position.here(pos))
}
else (thy, pos) })) })