# HG changeset patch
# User wenzelm
# Date 1567965872 -7200
# Node ID 7b6e6d61204a7ffe220878396a3d8aa32b3edf25
# Parent  36c8c32346cb4d3dbea13a02987e0415502f9050
clarified messages;

diff -r 36c8c32346cb -r 7b6e6d61204a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Sep 08 17:49:35 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Sep 08 20:04:32 2019 +0200
@@ -382,16 +382,23 @@
             val dir_errors =
             {
               val ok = (for { (dir, _) <- info.dirs } yield dir.canonical_file).toSet
-              (for {
+              val bad =
+                (for {
                   ((name, _), _) <- used_theories.iterator
                   if imports_base.theory_qualifier(name) == session_name
                   val path = name.master_dir_path
                   if !ok(path.canonical_file)
-                } yield {
-                  val path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
-                  "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
-                }
-              ).toList
+                  path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
+                } yield (path1, name)).toList
+              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).toSet.toList.sorted
+
+              val errs1 =
+                for { (path1, name) <- bad }
+                yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
+              val errs2 =
+                if (bad_dirs.isEmpty) Nil
+                else List("Implicit use of session directories: " + commas(bad_dirs))
+              errs1 ::: errs2
             }
 
             val sources_errors =