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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
