cache sources: invoke SHA1.digest at most once;
authorwenzelm
Sun Oct 01 17:59:26 2017 +0200 (18 months ago)
changeset 66743ff05d922bc34
parent 66742 b3422f78270e
child 66744 fec1504e5f03
cache sources: invoke SHA1.digest at most once;
maintain imported_sources, as required for new theories;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 01 16:56:47 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 17:59:26 2017 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4      known: Known = Known.empty,
     1.5      overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     1.6      sources: List[(Path, SHA1.Digest)] = Nil,
     1.7 +    imported_sources: List[(Path, SHA1.Digest)] = Nil,
     1.8      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
     1.9      errors: List[String] = Nil,
    1.10      imports: Option[Base] = None)
    1.11 @@ -143,13 +144,6 @@
    1.12      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.13    }
    1.14  
    1.15 -  private def check_files(paths: List[Path]): (List[(Path, SHA1.Digest)], List[String]) =
    1.16 -  {
    1.17 -    val digests = for (p <- paths if p.is_file) yield (p, SHA1.digest(p.file))
    1.18 -    val errors = for (p <- paths if !p.is_file) yield "No such file: " + p
    1.19 -    (digests, errors)
    1.20 -  }
    1.21 -
    1.22    sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
    1.23    {
    1.24      def is_empty: Boolean = session_bases.isEmpty
    1.25 @@ -179,6 +173,25 @@
    1.26        check_keywords: Set[String] = Set.empty,
    1.27        global_theories: Map[String, String] = Map.empty): Deps =
    1.28    {
    1.29 +    var cache_sources = Map.empty[JFile, SHA1.Digest]
    1.30 +    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
    1.31 +    {
    1.32 +      for {
    1.33 +        path <- paths
    1.34 +        file = path.file
    1.35 +        if cache_sources.isDefinedAt(file) || file.isFile
    1.36 +      }
    1.37 +      yield {
    1.38 +        cache_sources.get(file) match {
    1.39 +          case Some(digest) => (path, digest)
    1.40 +          case None =>
    1.41 +            val digest = SHA1.digest(file)
    1.42 +            cache_sources = cache_sources + (file -> digest)
    1.43 +            (path, digest)
    1.44 +        }
    1.45 +      }
    1.46 +    }
    1.47 +
    1.48      val session_bases =
    1.49        (Map.empty[String, Base] /: sessions.imports_topological_order)({
    1.50          case (session_bases, info) =>
    1.51 @@ -226,6 +239,8 @@
    1.52                  info.files.map(file => info.dir + file) :::
    1.53                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.54  
    1.55 +            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    1.56 +
    1.57              if (list_files)
    1.58                progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
    1.59  
    1.60 @@ -272,7 +287,8 @@
    1.61                  theories = thy_deps.names,
    1.62                  loaded_files = loaded_files)
    1.63  
    1.64 -            val (sources, sources_errors) = check_files(session_files)
    1.65 +            val sources_errors =
    1.66 +              for (p <- session_files if !p.is_file) yield "No such file: " + p
    1.67  
    1.68              val base =
    1.69                Base(
    1.70 @@ -281,7 +297,8 @@
    1.71                  loaded_theories = thy_deps.loaded_theories,
    1.72                  known = known,
    1.73                  overall_syntax = overall_syntax,
    1.74 -                sources = sources,
    1.75 +                sources = check_sources(session_files),
    1.76 +                imported_sources = check_sources(imported_files),
    1.77                  session_graph = session_graph,
    1.78                  errors = thy_deps.errors ::: sources_errors,
    1.79                  imports = Some(imports_base))
     2.1 --- a/src/Pure/Thy/thy_info.scala	Sun Oct 01 16:56:47 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Sun Oct 01 17:59:26 2017 +0200
     2.3 @@ -66,6 +66,17 @@
     2.4            names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     2.5      }
     2.6  
     2.7 +    def imported_files: List[Path] =
     2.8 +    {
     2.9 +      val base = resources.session_base
    2.10 +      val base_theories =
    2.11 +        loaded_theories.all_preds(names.map(_.theory)).
    2.12 +          filter(base.loaded_theories.defined(_))
    2.13 +
    2.14 +      base_theories.map(theory => base.known.theories(theory).path) :::
    2.15 +      base_theories.flatMap(base.known.loaded_files(_))
    2.16 +    }
    2.17 +
    2.18      lazy val overall_syntax: Outer_Syntax =
    2.19        Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    2.20