Thanks for the information, Mathias
> On 4 Nov 2015, at 15:55, Makarius <makar...@sketis.net> wrote: > > On Wed, 4 Nov 2015, Mathias Fleury wrote: > >> I am a bit surprised that the content of the tooltips and the output panel >> can be changed (both in 6d513469f9b2 and Isabelle_23-Oct-2015). >> >> Step to reproduce: >> * open a theory file >> * type a lemma >> * select some text of the output panel >> * type any letter >> >> Result: the selected text is gone and replaced by what has been typed. >> Expected: the output panel should not be changed. > > This odd behaviour stems from d40f906bb13f, which is the update to > jedit-5.3.0. The jedit-changes file says: > > - Allow editing, but not saving, of read only files. > (Feature request #422 - Dale Anson) > > The corresponding tracker item > http://sourceforge.net/p/jedit/feature-requests/422 reads like this: > > Jedit must allow user to make edits in a readonly files. It is very > wrong to disable this in any case: jedit is the _text editor_ > > Just from the wording, the feature request was formally wrong, and would not > have gone through on any Isabelle mailing list. > > > This incident means I need to figure out a different way to avoid edits on > output-only text areas. > > > Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev