# HG changeset patch
# User wenzelm
# Date 1504614583 -7200
# Node ID 1af360d1cad257a3302621ee9f9bed14d4476c96
# Parent  f6a1274be674bddb3e196d9c640c4404863b7b70
tolerate more errors (cf. 1e5ae735e026);

diff -r f6a1274be674 -r 1af360d1cad2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 04 20:55:06 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 05 14:29:43 2017 +0200
@@ -251,6 +251,11 @@
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
+            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 base =
               Base(
                 pos = info.pos,
@@ -260,9 +265,9 @@
                 known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
                 keywords = thy_deps.keywords,
                 syntax = syntax,
-                sources = all_files.map(p => (p, SHA1.digest(p.file))),
+                sources = sources,
                 session_graph = session_graph,
-                errors = thy_deps.errors)
+                errors = thy_deps.errors ::: sources_errors)
 
             session_bases + (info.name -> base)
           }