[isabelle-dev] Feature suggestion: apply (meth[1!])

[Makarius]

On Mon, 11 Mar 2013, Joachim Breitner wrote:

> This lets you say "assert_goals 5" in your apply scripts where you think
> there should be 5 goals.

Of course there is always a possibility to devise new commands.  Critical 
review will only start when such things show up in publicly accessible 
Isabelle example sessions, or even the main code base.

You can also experiment with something similar as proof method: there is 
no problem to emit warnings, and then do nothing.  You only need to look 
thrice how it generally interacts with the lazy enumeration scheme of goal 
states in method expressions (including backtracking).


> If that is not the case, then jEdit shows some red wiggles, but 
> otherwise allows you to continue as before.

That aspect is just an accident of the very weak "error recovery" of the 
interactive document processing.  After the next round of reforms, an 
unstructured apply script will stop after the first failed command -- at 
that level of nested proof structure.

Getting that right has much higher priority than adding features 
elsewhere.


 	Makarius