[isabelle-dev] Annotations in Theories panel not visible

Lars Noschinski noschinl at in.tum.de
Tue Apr 1 07:54:14 CEST 2014


On 31.03.2014 22:43, Makarius wrote:
> On Tue, 18 Mar 2014, Lars Noschinski wrote:
>
>> I just noticed (in f0d2609c4cdc) that not all warnings and errors are
>> visible in the Theories panel. If I run
>>
>>   isabelle jedit -l Pure src/Pure/Main.thy
>>
>> and watch the Theories panel, I see that there are some warning e.g. in
>> Orderings. However, as soon as Orderings is finished, the annotations
>> for Orderings disappear (in the Theories panel). This happens with some,
>> but not all theories (e.g., Code_Generator or Ctr_Sugar keep their
>> annotations). This happens not only for warnings, but also for errors.
>
> Thanks for keeping an eye on such important details. Did you see this
> again in the meantime?  I could not reproduce it in the version
> f0d2609c4cdc nor in 97d6a786e0f9 from today.
Reproducable with 97d6a786e0f9.
>
> Theory Orderings has very few warnings compared to Code_Generator or
> Ctr_Sugar, so there could be a problem with the GUI geometry
> calculations. These are just small rectangles painted in a certain
> spot -- when the theory is finished the odd messages move to the right
> and might just get out of view.
Looking at the problem more closely, it seems that the final rectangles
(after the theory has finished) are about half or maybe a third the size
of the rectangles during processes (and vanish, if they are small enough).
>
> I've tried on Linux with Swing L&F Nimbus, GTK+, Metal, and it all
> works for me.
>
> Do you have any special GUI or font properties?  If the problem still
> persists can you make a screenshot?
I made a short video:
<http://www21.in.tum.de/~noschinl/jedit-annotations.webm>.

I tested the Metal and Nimbus L&F; the font is IsabelleText. This is on
a system running Debian stable with Gnome 3.4.2.

I couldn't reproduce the behaviour on another machine with Debian
testing and Gnome 3.8.4.

  -- Lars


More information about the isabelle-dev mailing list