[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