[isabelle-dev] sledgehammer panel problem

[Makarius]

On Mon, 16 Sep 2013, Lawrence Paulson wrote:

> Any generated "metis" calls only self-insert if clicked before s/h 
> terminates. If you ignore your session for a few minutes while s/h runs 
> (as many people do), then the highlighted links will be inactive when 
> you get back. I've checked this several times.

The "sendback" text addresses a particular command in the text, if that is 
destroyed by editing, it will not work.

Part of the problem is the old debate what a command span really is.  1.5 
years ago I've broken with ancient traditions and lessons learned from 
Proof General and *included* trailing whitespace/comments here.  This had 
a slight advantage in the total number of command transactions.

Many other surprises were coming from it, though.  Here the snag is that 
appending something after a command affects its trailing white space and 
thus resets it.


In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* 
trailing whitespace/comments and make a separate "ignored" command span 
instead.  The notion of "current_command" for Output and query operations 
like Find or Sledgehammer is adapted accordingly.

So the command where sledgehammer is applied is now more robust against 
edits of the surrounding text.  Hopefully this scheme is sufficient for 
this release.


 	Makarius