[isabelle-dev] Update of jdk and jedit components

[Makarius]

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