Re: [isabelle] replace "isabelle tty"

On Fri, 21 Nov 2014, Walther Neuper wrote:

 I suppose this could be extended to support a "go-back" or even
 some more complicated protocol like the one from ProofGeneral
 which I presume you are currently using.
... we have an even simpler protocol than ProofGeneral, so your solution would be quite appropriate for a quick shortcut.

Such a shortcut would be necessary, if the efforts required for a solution via Isabelle/Scala would be beyond our present resources.

The problem posed here is technically trivial, i.e. a non-problem. It is just a matter to overcome old ways of thinking about it.

Isabelle/Scala is well-established as the main system programming interface for several years. When you want to connect to some Isabelle prover process, the Scala APIs are the way to do it.

Pretty soon, it will be no longer possible to use the Isabelle process at all, without the Scala process around it. The remaining TTY loop was hindering important reforms long enough. After Isabelle2014 it is no longer there, without any traces of it left.

Then it becomes possible to assume that things like Invoke_Scala.method work in Isabelle/ML all the time, and many problems from the past can be resolved in the proper way. (E.g. a brushed-up version of document preparation.)


           927,487 people so far

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