Re: [isabelle] Interfacing with Isabelle



Well, your ML function does not have to terminate immediately. The setup for Proof General for example takes over the tty and then reacts to further input. All of this is very delicate to get right, though. Better try something based on the new process wrapper.

I've found the grammar for the Isabelle input syntax, but I have yet to find one for the Isabelle output. Does one exist that you know of? It seems this would be crucial for the creation of higher levels of control on top of what Isabelle offers.


Regards,
Scott





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