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 <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
