Re: [isabelle-dev] sledgehammer panel problem
On Tue, 24 Sep 2013, Lawrence Paulson wrote: 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. Now I understand what you mean. I've addresses this here: changeset: 53867:6e69f9ca8f1c user:wenzelm date:Wed Sep 25 11:12:59 2013 +0200 files: src/Pure/PIDE/query_operation.scala src/Tools/jEdit/src/find_dockable.scala src/Tools/jEdit/src/sledgehammer_dockable.scala description: explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d); Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Wed, 25 Sep 2013, Lawrence Paulson wrote: I seem to be having problems with this version (f54a8f591e0f). I tried the usual tricks but I still get compilation errors. ~/isabelle/hfinite/Incompleteness: isabelle jedit -f SyntaxN.thy ### Building Isabelle/Scala ... GUI/gui.scala:47: error: not found: value split_lines if (height 0 split_lines(txt).length height) text.rows = height ^ Tools/main.scala:140: error: not found: value quote error(Bad Isabelle home directory: + quote(isabelle_home)) ^ 83 errors found Failed to compile sources ~/isabelle/hfinite/Incompleteness: hg id f54a8f591e0f tip I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
Sorry 7cec5a4d5532 Deleting Isabelle/lib/classes did the trick. Larry On 25 Sep 2013, at 14:58, Makarius makar...@sketis.net wrote: I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
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
Re: [isabelle-dev] sledgehammer panel problem
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
