# HG changeset patch
# User wenzelm
# Date 1595595736 -7200
# Node ID 4768b1facec2367417ff61d26011f37979b67505
# Parent  17507b48b6f52555a6615ce967d377cf532379e4
clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);

diff -r 17507b48b6f5 -r 4768b1facec2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Jul 24 12:15:37 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Jul 24 15:02:16 2020 +0200
@@ -166,9 +166,13 @@
             val overall_syntax = dependencies.overall_syntax
 
             val theory_files = dependencies.theories.map(_.path)
-            val loaded_files =
-              if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name))
-              else Nil
+
+            val (loaded_files, loaded_files_errors) =
+              try {
+                if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
+                else (Nil, Nil)
+              }
+              catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
@@ -299,8 +303,8 @@
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
-                errors = dependencies.errors ::: import_errors ::: dir_errors :::
-                  sources_errors ::: path_errors ::: bibtex_errors)
+                errors = dependencies.errors ::: loaded_files_errors ::: import_errors :::
+                  dir_errors ::: sources_errors ::: path_errors ::: bibtex_errors)
 
             session_bases + (info.name -> base)
           }