[isabelle-dev] NEWS: "isabelle tty" is superseded by "isabelle console"
makarius at sketis.net
Mon Jun 30 12:11:55 CEST 2014
* 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
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.
More information about the isabelle-dev