[isabelle-dev] Find theorems and Sledgehammer Panels

Makarius makarius at sketis.net
Tue Sep 24 22:04:05 CEST 2013

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, but there were people in the past who have 
seen them.  According to some Mark Swingler, Java Runtime Engineer at 
Apple Inc. in 2008, the Java Mac OS X look-and-feel *has* to select all 
text after change of focus of the GUI component.

So despite roaring crowds on the Web shouting "bug", this behaviour is 
normal.  The business model of Mac OS X is to be different.  (Linux 
communities are different without a business model behind it.)

Luckily there was also an explanation by the same guy how to disable 
normal Apple behaviour and imitate Linux and Windows.  Thus our text field 
completion becomes more usable in Isabelle/8d7029eb0c31.

Software development in the 21fst century is a strange adventure game, 
where one needs to solve quests in dark places ...


More information about the isabelle-dev mailing list