On Fri, 4 Dec 2015, Dmitriy Traytel wrote:
here is one way to still (e1e6bb36b27a) edit the output buffer: to use
the compose key.
On my Mac, if I place the cursor into the output buffer and press alt-u
followed bei u, an ü appears in the output.
See now
changeset: 62211:451bd09b8277
user: wenzelm
date: Wed Jan 20 19:19:33 2016 +0100
files: src/Tools/jEdit/src/pretty_text_area.scala
description:
bypass input method for better imitation of read-only mode (cf.
f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;
This is also relevant to popups: here the focus policy is a bit different.
The compose-sequence above should produce a prop "ü", but blindly without
showing the intermediate state.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
