[isabelle-dev] Update of jdk and jedit components
traytel at inf.ethz.ch
Fri Dec 4 16:42:22 CET 2015
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.
> On 04 Nov 2015, at 20:42, Makarius <makarius at sketis.net> wrote:
> On Wed, 4 Nov 2015, Makarius wrote:
>> This incident means I need to figure out a different way to avoid edits on output-only text areas.
> See now
> changeset: 61570:f26a4d5e82b5
> user: wenzelm
> date: Wed Nov 04 17:14:17 2015 +0100
> files: src/Tools/jEdit/src/pretty_text_area.scala
> dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev