[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 ...
Makarius
More information about the isabelle-dev
mailing list