# HG changeset patch
# User wenzelm
# Date 1595585737 -7200
# Node ID 17507b48b6f52555a6615ce967d377cf532379e4
# Parent  ba5b3767152827f7a00aa3e4adb4f459538d1054
clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");

diff -r ba5b37671528 -r 17507b48b6f5 src/Pure/Thy/sessions.scala
--- 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)
           }