# HG changeset patch
# User wenzelm
# Date 1506873566 -7200
# Node ID ff05d922bc3435efa84412669f46a022b89b070f
# Parent  b3422f78270ea821c57a677fc6f2932eab9e10fa
cache sources: invoke SHA1.digest at most once;
maintain imported_sources, as required for new theories;

diff -r b3422f78270e -r ff05d922bc34 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Oct 01 16:56:47 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 17:59:26 2017 +0200
@@ -115,6 +115,7 @@
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
+    imported_sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil,
     imports: Option[Base] = None)
@@ -143,13 +144,6 @@
     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
@@ -179,6 +173,25 @@
       check_keywords: Set[String] = Set.empty,
       global_theories: Map[String, String] = Map.empty): Deps =
   {
+    var cache_sources = Map.empty[JFile, SHA1.Digest]
+    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
+    {
+      for {
+        path <- paths
+        file = path.file
+        if cache_sources.isDefinedAt(file) || file.isFile
+      }
+      yield {
+        cache_sources.get(file) match {
+          case Some(digest) => (path, digest)
+          case None =>
+            val digest = SHA1.digest(file)
+            cache_sources = cache_sources + (file -> digest)
+            (path, digest)
+        }
+      }
+    }
+
     val session_bases =
       (Map.empty[String, Base] /: sessions.imports_topological_order)({
         case (session_bases, info) =>
@@ -226,6 +239,8 @@
                 info.files.map(file => info.dir + file) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
+            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
+
             if (list_files)
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
 
@@ -272,7 +287,8 @@
                 theories = thy_deps.names,
                 loaded_files = loaded_files)
 
-            val (sources, sources_errors) = check_files(session_files)
+            val sources_errors =
+              for (p <- session_files if !p.is_file) yield "No such file: " + p
 
             val base =
               Base(
@@ -281,7 +297,8 @@
                 loaded_theories = thy_deps.loaded_theories,
                 known = known,
                 overall_syntax = overall_syntax,
-                sources = sources,
+                sources = check_sources(session_files),
+                imported_sources = check_sources(imported_files),
                 session_graph = session_graph,
                 errors = thy_deps.errors ::: sources_errors,
                 imports = Some(imports_base))
diff -r b3422f78270e -r ff05d922bc34 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Sun Oct 01 16:56:47 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Sun Oct 01 17:59:26 2017 +0200
@@ -66,6 +66,17 @@
           names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     }
 
+    def imported_files: List[Path] =
+    {
+      val base = resources.session_base
+      val base_theories =
+        loaded_theories.all_preds(names.map(_.theory)).
+          filter(base.loaded_theories.defined(_))
+
+      base_theories.map(theory => base.known.theories(theory).path) :::
+      base_theories.flatMap(base.known.loaded_files(_))
+    }
+
     lazy val overall_syntax: Outer_Syntax =
       Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))