clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
--- a/src/Pure/Thy/sessions.scala Thu Jul 23 22:32:06 2020 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Jul 24 12:15:37 2020 +0200
@@ -232,6 +232,18 @@
val used_theories_session =
dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
+ val import_errors =
+ {
+ val known_sessions =
+ sessions_structure.imports_requirements(List(session_name)).toSet
+ for {
+ name <- dependencies.theories
+ qualifier = deps_base.theory_qualifier(name)
+ if !known_sessions(qualifier)
+ } yield "Bad import of theory " + quote(name.toString) +
+ ": need to include sessions " + quote(qualifier) + " in ROOT"
+ }
+
val dir_errors =
{
val ok = info.dirs.map(_.canonical_file).toSet
@@ -287,8 +299,8 @@
imported_sources = check_sources(imported_files),
sources = check_sources(session_files),
session_graph_display = session_graph_display,
- errors = dependencies.errors ::: dir_errors ::: sources_errors :::
- path_errors ::: bibtex_errors)
+ errors = dependencies.errors ::: import_errors ::: dir_errors :::
+ sources_errors ::: path_errors ::: bibtex_errors)
session_bases + (info.name -> base)
}