Ant S. (Jun 22 2026 at 09:55): Ant S. (Jun 22 2026 at 09:55):Suppose I have a session foo. isabelle build allows me to build this session. I can also load this session into jEdit but it seems that I cannot work in this session once it is built. For that, I have to switch into draft mode.
Suppose further that I have three theories, namely: theory1, theory2 and theory3 as part of this session, and that theory2 imports theory1. If I want to refer to theory1 by name, it would be @{theory Draft.theory1} while developing, but @{theory foo.theory1} when building the session, since @{theory Draft.theory1} doesn't exist at this point. Outside of a sed script when running isabelle build, is there some way to handle this nicely between when I'm developing a theory and building one?
Or am I understanding sessions incorrectly? Reading the Isar reference manual, is this what a generic context is for?
Ant S. (Jun 22 2026 at 09:55):(or am I just misunderstanding how to use sessions)
Fabian Huch (Jun 22 2026 at 10:29):You are mixing up concepts: Build vs. Interactive session, Draft Session vs Defined session.
Ie, you should load your session properly when editing, e.g. with the -R flag of Isabelle/jEdit
Ant S. (Jun 22 2026 at 10:45):oh i see, I guess I should stare at the isar ref manual more carefully
Ant S. (Jun 22 2026 at 10:45):thanks!
Last updated: Jun 26 2026 at 21:20 UTC