[isabelle-dev] sledgehammer panel problem

Makarius makarius at sketis.net
Wed Sep 25 13:00:05 CEST 2013


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



More information about the isabelle-dev mailing list