Re: [isabelle-dev] sledgehammer panel problem

2013-09-25 Thread Makarius
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

Re: [isabelle-dev] sledgehammer panel problem

2013-09-25 Thread Makarius
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:

Re: [isabelle-dev] sledgehammer panel problem

2013-09-25 Thread Lawrence Paulson
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

Re: [isabelle-dev] sledgehammer panel problem

2013-09-24 Thread 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

Re: [isabelle-dev] sledgehammer panel problem

2013-09-24 Thread 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