[isabelle-dev] Find theorems and Sledgehammer Panels
makarius at sketis.net
Mon Sep 23 15:03:48 CEST 2013
On Thu, 5 Sep 2013, Christian Sternagel wrote:
> Last time I tried, there was no auto completion available in the input
> of the find theorem panel. Which makes the variant of typing
> find_theorems yourself in the main buffer more convenient for me at the
With Isabelle/322a3ff42b33 there is now completion for the history text
field behind it.
It is again one of these typical instances of spending 2h to make it work
on Linux and Windows, and requiring days or weeks to find out why
Apple/Oracle don't quite manage on Mac OS X: the focus change after
completion selects all text. (Problem still pending.)
> Also I experienced already several "hangs" with this panel as well as
> the sledgehammer panel. For the former that means that even after
> waiting for a long time nothing shows up, whereas for the latter the
> whole main buffer stays in a grayish highlighted state and does no
> longer produce output in response to edits (and also doesn't respond to
> clicking cancel).
This sounds again like a total-existence-failure due on Fedora. Was "last
time I tried" already on jdk-7u40? Just a straw of hope ...
More information about the isabelle-dev