* Former "isabelle tty" has been superseded by "isabelle console",
with implicit build like "isabelle jedit", and without the mostly
obsolete Isar TTY loop.
This refers to Isabelle/0e41f26a0250. Recently, I've found myself more
often doing an 'exit' of the Isar loop of "isabelle tty" instead of
actually using it.
Note that low-level system tinkering of the Isar toplevel may be done with
ML use_thy and an auxiliary .thy file, potentially together with
Toplevel.interactive := true for precise imitation of that "mode", which
often causes the actual problems in the first-place. (I hardly do that
myself, though, but use the Prover IDE directly for debugging and
tinkering.)
Are there any remaining uses of the Isar toplevel? Otherwise it is
something to be scheduled for eventual removal -- it complicates many
aspects of the system.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
