Changes

Summary

1. tuned imports;
2. always explore all sessions;
3. optionally explore all sessions -- potentially slow, e.g. for AFP;
4. proper sections;
5. clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
6. proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
7. clarified session graph: collapse theories from other sessions;
8. more robust error (amending 2c27c3d1fd3b): responsibility is gradually moved from ML to Scala;
9. exclude theories from other sessions; clarified modules;
10. some documentation;
11. actually qualify theory names;