src/Pure/Thy/sessions.scala
changeset 66742 b3422f78270e
parent 66737 2edc0c42c883
child 66743 ff05d922bc34
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 01 15:17:43 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 16:56:47 2017 +0200
     1.3 @@ -143,6 +143,13 @@
     1.4      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
     1.5    }
     1.6  
     1.7 +  private def check_files(paths: List[Path]): (List[(Path, SHA1.Digest)], List[String]) =
     1.8 +  {
     1.9 +    val digests = for (p <- paths if p.is_file) yield (p, SHA1.digest(p.file))
    1.10 +    val errors = for (p <- paths if !p.is_file) yield "No such file: " + p
    1.11 +    (digests, errors)
    1.12 +  }
    1.13 +
    1.14    sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
    1.15    {
    1.16      def is_empty: Boolean = session_bases.isEmpty
    1.17 @@ -197,14 +204,9 @@
    1.18              }
    1.19  
    1.20              val thy_deps =
    1.21 -            {
    1.22 -              val root_theories =
    1.23 -                info.theories.flatMap({ case (_, thys) =>
    1.24 -                  thys.map({ case (thy, pos) =>
    1.25 -                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
    1.26 -                })
    1.27 -              resources.thy_info.dependencies(root_theories)
    1.28 -            }
    1.29 +              resources.thy_info.dependencies(
    1.30 +                for { (_, thys) <- info.theories; (thy, pos) <- thys }
    1.31 +                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
    1.32  
    1.33              val overall_syntax = thy_deps.overall_syntax
    1.34  
    1.35 @@ -219,13 +221,13 @@
    1.36                }
    1.37                else Nil
    1.38  
    1.39 -            val all_files =
    1.40 +            val session_files =
    1.41                (theory_files ::: loaded_files.flatMap(_._2) :::
    1.42                  info.files.map(file => info.dir + file) :::
    1.43                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.44  
    1.45              if (list_files)
    1.46 -              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.47 +              progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
    1.48  
    1.49              if (check_keywords.nonEmpty) {
    1.50                Check_Keywords.check_keywords(
    1.51 @@ -270,10 +272,7 @@
    1.52                  theories = thy_deps.names,
    1.53                  loaded_files = loaded_files)
    1.54  
    1.55 -            val sources =
    1.56 -              for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
    1.57 -            val sources_errors =
    1.58 -              for (p <- all_files if !p.is_file) yield "No such file: " + p
    1.59 +            val (sources, sources_errors) = check_files(session_files)
    1.60  
    1.61              val base =
    1.62                Base(