*** General *** * Session ROOT files need to specify explicit 'directories' for import of theory files. Directories cannot be shared by different sessions. (Recall that import of theories from other sessions works via session-qualified theory names, together with suitable 'sessions' declarations in the ROOT.)
*** Isabelle/jEdit Prover IDE *** * Prover IDE startup is now much faster, because theory dependencies are no longer explored in advance. The overall session structure with its declarations of 'directories' is sufficient to locate theory files. Thus the "session focus" of option "isabelle jedit -S" has become obsolete (likewise for "isabelle vscode_server -S"). Existing option "-R" is both sufficient and more convenient to start editing a particular session. *** System *** * The command-line tool "isabelle imports" has been discontinued: strict checking of session directories enforces session-qualified theory names in applications -- users are responsible to specify session ROOT entries properly. This refers to Isabelle/9cde8c4ea5a5 and AFP/98320942654a. It means that session directories are much better defined than ever before, and the overall session/theory management has become more robust and faster. The scheme turned out a bit more liberal than I anticipated some years ago: it is still possible to have multiple directories for a single session, even though this often obscures its content. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev