Re: [isabelle] replace "isabelle tty"
thank you for the surprising mini-solution ...
On 14-11-21 04:46 PM, Cezary Kaliszyk wrote:
... we have an even simpler protocol than ProofGeneral, so your solution
would be quite appropriate for a quick shortcut.
The script runs:
Then sends it:
"val s = Toplevel.toplevel;"
And for every line of user input sends:
"val s = fold (Toplevel.command_exception true) (Outer_Syntax.parse
Position.start \"%s\") s;"
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.
Such a shortcut would be necessary, if the efforts required for a
solution via Isabelle/Scala would be beyond our present resources.
So, probably we come back to your solution after some trials.
This archive was generated by a fusion of
Pipermail (Mailman edition) and