HomeIsabelle/Phabricator

clarified errors: avoid hiding of import_errors/dir_errors by their…

Authored by makarius.

Description

clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);

Details