# HG changeset patch
# User wenzelm
# Date 1568669109 -7200
# Node ID b3f61e166763b4d8ef6fee95fd8f9a47030448fd
# Parent  5bb025e24224180d43b764132d49aa6ad54250c8
more errors;

diff -r 5bb025e24224 -r b3f61e166763 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 16 23:20:45 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 16 23:25:09 2019 +0200
@@ -312,14 +312,19 @@
               for ((options, name) <- dependencies.adjunct_theories)
               yield (name, options)
 
+            def used_theories_session_iterator: Iterator[Document.Node.Name] =
+              for {
+                (name, _) <- used_theories.iterator
+                if imports_base.theory_qualifier(name) == session_name
+              } yield name
+
             val dir_errors =
             {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
-                  (name, _) <- used_theories.iterator
-                  if imports_base.theory_qualifier(name) == session_name
-                  val path = name.master_dir_path
+                  name <- used_theories_session_iterator
+                  path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
@@ -332,8 +337,15 @@
                 if (bad_dirs.isEmpty) Nil
                 else List("Implicit use of session directories: " + commas(bad_dirs))
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
+              val errs4 =
+                (for {
+                  name <- used_theories_session_iterator
+                  name1 <- resources.find_theory_node(name.theory)
+                  if name.node != name1.node
+                } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
+                .toList
 
-              errs1 ::: errs2 ::: errs3
+              errs1 ::: errs2 ::: errs3 ::: errs4
             }
 
             val sources_errors =