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
