Re: [isabelle-dev] Annotations in Theories panel not visible
On Tue, 1 Apr 2014, Lars Noschinski wrote: I made a short video: http://www21.in.tum.de/~noschinl/jedit-annotations.webm. I tested the Metal and Nimbus LF; 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. Looking closer yet again, the annotations don't vanish, but the bars get too wide. If you look at the video above, the Theories panel is redrawn two times before the actual process of proving starts. Each time, the width of the bars increases. After the third iteration, it is wider than the panel. But there is no optical indication for this (e.g., a scrollbar), so it looks like part of the annotations vanish when processing procedes into the hidden part of the panel. The video is very helpful, it shows the dynamics of what is really going on. My initial reaction (without much thinking) was to resize the Theories dockable, since I am used to Swing components not being very precise concerning scrollbars etc. (this also depends on LF). I don't know an easy way to combine scrollbars with flexible (two-dimensional) layouts, as seen in this list view. A more basic approach is now in Isabelle/8a58a8c5a1c0, just painting more borders. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Annotations in Theories panel not visible
On 01.04.2014 07:54, Lars Noschinski wrote: I've tried on Linux with Swing LF 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 LF; 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. Looking closer yet again, the annotations don't vanish, but the bars get too wide. If you look at the video above, the Theories panel is redrawn two times before the actual process of proving starts. Each time, the width of the bars increases. After the third iteration, it is wider than the panel. But there is no optical indication for this (e.g., a scrollbar), so it looks like part of the annotations vanish when processing procedes into the hidden part of the panel. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Annotations in Theories panel not visible
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. 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. I've tried on Linux with Swing LF 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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Annotations in Theories panel not visible
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 LF 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 LF; 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Annotations in Theories panel not visible
Hi, 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. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
