Re: [isabelle] replace "isabelle tty"



Dear Cezary,

thank you for the surprising mini-solution ...

On 14-11-21 04:46 PM, Cezary Kaliszyk wrote:
The script runs:
   "isabelle console",
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.
... 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.

So, probably we come back to your solution after some trials.

Regards,
Walther





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