[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