Re: [isabelle] replace "isabelle tty"



> Isabelle/Scala is indeed the main system programming language for
> Isabelle, so the manual should say more about it.  The reason why so
> little Isabelle/Scala is in the manuals is that code snippets cannot be
> formally checked, as is done for Isabelle/ML. Without formal checking,
> it is pointless to make examples, because they will stop working in no
> time, after the next round of refinements of the system implementation.

Indeed.

What could be done is writing a minimal PIDE application demonstrating
bi-directional communication, possibly in the style of literate
programming. This could then be executed and tested as part of a regular
(nightly?) build against the repository version.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.