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
