On Fri, 4 Dec 2015, Dmitriy Traytel wrote:
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.
See now
changeset: 62211:451bd09b8277
use
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 wrote:
>
> On Wed, 4 Nov 2015
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.sca
Thanks for the information,
Mathias
> On 4 Nov 2015, at 15:55, Makarius 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 reprod
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 lett
Hello Makarius,
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
In Isabelle/d40f906bb13f there is now jdk-8u66 and jedit-5.3.0. There are
relatively few changes from upstream; this is mainly consolidation.
As we are slowly approaching the pre-release mode, it is important to keep
an eye an all the fine points on all platforms. Does Java 8 really work
as
