tolerate more errors (cf. 1e5ae735e026);
authorwenzelm
Tue Sep 05 14:29:43 2017 +0200 (21 months ago)
changeset 666041af360d1cad2
parent 66603 f6a1274be674
child 66605 261dcd52c5a0
child 66606 f23f044148d3
tolerate more errors (cf. 1e5ae735e026);
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Sep 04 20:55:06 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Sep 05 14:29:43 2017 +0200
     1.3 @@ -251,6 +251,11 @@
     1.4                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
     1.5              }
     1.6  
     1.7 +            val sources =
     1.8 +              for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
     1.9 +            val sources_errors =
    1.10 +              for (p <- all_files if !p.is_file) yield "No such file: " + p
    1.11 +
    1.12              val base =
    1.13                Base(
    1.14                  pos = info.pos,
    1.15 @@ -260,9 +265,9 @@
    1.16                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.17                  keywords = thy_deps.keywords,
    1.18                  syntax = syntax,
    1.19 -                sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.20 +                sources = sources,
    1.21                  session_graph = session_graph,
    1.22 -                errors = thy_deps.errors)
    1.23 +                errors = thy_deps.errors ::: sources_errors)
    1.24  
    1.25              session_bases + (info.name -> base)
    1.26            }