Summary
- proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
- clarified session graph: collapse theories from other sessions;
- more robust error (amending 2c27c3d1fd3b): responsibility is gradually moved from ML to Scala;
- exclude theories from other sessions; clarified modules;
- some documentation;
- actually qualify theory names;
The file was modified | src/Pure/theory.ML (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Thy/thy_info.scala (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Doc/System/Sessions.thy (diff) |
The file was modified | src/Pure/PIDE/resources.ML (diff) |
The file was modified | src/Pure/ROOT.ML (diff) |
The file was modified | src/Pure/Thy/present.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Doc/System/Sessions.thy (diff) |
The file was modified | src/Pure/PIDE/resources.ML (diff) |
The file was modified | src/Pure/PIDE/resources.scala (diff) |