[isabelle-dev] Update of jdk and jedit components

[Dmitriy Traytel]

Hi Makarius,

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.

Dmitriy

> 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
> description:
> dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev