Changes

Summary

1. follow Phabricator update 2020 Week 27;
2. tuned;
3. unused;
4. clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);
5. clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");
6. clarified signature;
7. clarified order --- proper sorting of requirements;
8. obsolete (see 9cde8c4ea5a5);
9. tuned --- based on hints by IntelliJ;
10. tuned signature;