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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and