[isabelle-dev] Find theorems and Sledgehammer Panels

Makarius makarius at sketis.net
Wed Sep 25 23:55:26 CEST 2013


On Tue, 24 Sep 2013, Makarius wrote:

> On Mon, 23 Sep 2013, Makarius wrote:
>
>> 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.)
>
> Apple makes it more difficult to get into its dungeons where the real sources 
> are guarded by dragons

I need to correct this.  The formerly secret Apple sources are part of the 
regular Oracle JDK source forest, e.g. here:

   http://hg.openjdk.java.net/jdk7u/jdk7u-osx/jdk/file/tip/src/macosx/classes/com/apple

This might eventually give some insight into the important com.apple.laf 
and com.apple.eawt packages.


 	Makarius



More information about the isabelle-dev mailing list