On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote:
in a39250169636, it is possible to increase/decrease the font size in
jedit with cmd+<+>/cmd+<-> on MacOS (probably ctrl+<+>/ctrl+<-> on other
plattforms) (nice feature!). However, pressing cmd+<+> increases the
font size twice on my machine (cmd+<-> works fine).
That was one such convenience that I managed to get working after 20min
Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that
is not finished yet, and there are remaining problems to treat CTRL, ALT,
COMMAND modifiers properly: it can cause duplication or triplication of
key events.
See also the mail thread on "Mac OS X support on Oracle Java 7" that
Fabian Immler has started recently
http://sourceforge.net/mailarchive/message.php?msg_id=30165793
It touches some of the internal issues, including a slightly odd
workaround by myself to modify an older workaround to make it half-working
again under Java 7.
This needs more systematic investigation, by instrumenting the jEdit
sources to produce detailed traces for all critical points where the
MacOSX specific key handling happens. Then it needs to be compared for
Java 6 vs. Java 7, to reconstruct the ideas behind it, which nobody
seems to remember on jedit-devel.
I am unsure if I will manage anything like that myself before the Isabelle
release. Mac OS X poses a bit too many extra problems, and has a bit too
few people actually supporting it actively. On jedit-devel there is right
now exactly one Mac OS X guy hanging around.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
