[isabelle-dev] NEWS: "isabelle tty" is superseded by "isabelle console"

[Makarius]

* 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