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