[isabelle-dev] Find theorems and Sledgehammer Panels

[Makarius]

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 
> moment.

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 ...


 	Makarius