[isabelle-dev] sledgehammer panel problem

[Lawrence Paulson]

Thanks for the response, but my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that "sendback" does not work. So I'm force to watch s/h and choose one of the metis calls before s/h terminates. 

Larry

On 24 Sep 2013, at 20:52, Makarius <makarius at sketis.net> wrote:

> 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