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
