src/Pure/Thy/sessions.scala

         yield (theory, node_name.node)
 
     def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   }
 
+  private def check_files(paths: List[Path]): (List[(Path, SHA1.Digest)], List[String]) =
+  {
+    val digests = for (p <- paths if p.is_file) yield (p, SHA1.digest(p.file))
+    val errors = for (p <- paths if !p.is_file) yield "No such file: " + p
+    (digests, errors)
+  }
+
   sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
   {
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
     def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)

                 else info.groups.mkString(" (", " ", ")")
               progress.echo("Session " + info.chapter + "/" + info.name + groups)
             }
 
             val thy_deps =
-            {
-              val root_theories =
-                info.theories.flatMap({ case (_, thys) =>
-                  thys.map({ case (thy, pos) =>
-                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
-                })
-              resources.thy_info.dependencies(root_theories)
-            }
+              resources.thy_info.dependencies(
+                for { (_, thys) <- info.theories; (thy, pos) <- thys }
+                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
 
             val overall_syntax = thy_deps.overall_syntax
 
             val theory_files = thy_deps.names.map(_.path)
             val loaded_files =

                 }
                 else thy_deps.loaded_files
               }
               else Nil
 
-            val all_files =
+            val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.files.map(file => info.dir + file) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
             if (list_files)
-              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
+              progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }

             val known =
               Known.make(info.dir, List(imports_base),
                 theories = thy_deps.names,
                 loaded_files = loaded_files)
 
-            val sources =
-              for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
-            val sources_errors =
-              for (p <- all_files if !p.is_file) yield "No such file: " + p
+            val (sources, sources_errors) = check_files(session_files)
 
             val base =
               Base(
                 pos = info.pos,
                 global_theories = global_theories,