Email Gateway (Aug 19 2022 at 10:32): Email Gateway (Aug 19 2022 at 10:32):From: Makarius <makarius@sketis.net>
I've learned a few more fine points about that in the past few days, so
the heuristics will approximate an actual solution eventually. That is
all for the next release though, and it is a bit early to speculate how it
will be there. (There are still many Java/Swing issues on various
platforms, some of them hard drop-outs due to Oracle.)
Makarius
Email Gateway (Aug 19 2022 at 10:45):From: John Wickerson <jpw48@cam.ac.uk>
Minor bug report (not sure if this is Isabelle's fault or jEdit's, but here goes)...
The word wrapping in the Output window of Isabelle/jEdit is a little bit off. That is, each line of text breaks about 1cm beyond the right-hand edge of the Output window (and that's independent of how I resize the window). Of course it's only a minor quibble because I can always scroll horizontally a little bit to see the rest of the output. It doesn't help to turn on/off the gutter.
john
Email Gateway (Aug 19 2022 at 10:45):From: Makarius <makarius@sketis.net>
I think you mean the breaking of pretty-printed formal output.
(Word-wrap in the source is a different issue: there is also a snag here,
because Isabelle tokenization for {* ... *} is in conflict with jEdit
tokenization for words.)
The font metrics and window size parameters for pretty printed output are
only precise once the inner GUI component geometry is known. It does not
quite work with extra decoration (scrollbars, window borders): before the
window is mapped these sizes are unknown, or I did not know how to get
them in Java/AWT/Swing.
So Isabelle2013 has some funny heuristics here that work for the most
common platforms, GUI look-and-feels, fonts, and font-sizes. What do you
have in this respect?
Makarius
Email Gateway (Aug 19 2022 at 10:45):From: John Wickerson <jpw48@cam.ac.uk>
On 13 Mar 2013, at 14:52, Makarius wrote:
On Wed, 13 Mar 2013, John Wickerson wrote:
The word wrapping in the Output window of Isabelle/jEdit is a little bit off. That is, each line of text breaks about 1cm beyond the right-hand edge of the Output window (and that's independent of how I resize the window). Of course it's only a minor quibble because I can always scroll horizontally a little bit to see the rest of the output. It doesn't help to turn on/off the gutter.
I think you mean the breaking of pretty-printed formal output. (Word-wrap in the source is a different issue: there is also a snag here, because Isabelle tokenization for {* ... *} is in conflict with jEdit tokenization for words.)
Yes, that's what I mean.
The font metrics and window size parameters for pretty printed output are only precise once the inner GUI component geometry is known. It does not quite work with extra decoration (scrollbars, window borders): before the window is mapped these sizes are unknown, or I did not know how to get them in Java/AWT/Swing.
So Isabelle2013 has some funny heuristics here that work for the most common platforms, GUI look-and-feels, fonts, and font-sizes. What do you have in this respect?
I'm on Mac OS 10.7.5, with "Swing look & feel" set to "Metal", font "IsabelleText 14 Plain". I've tried fiddling with each of these settings (well, except the OS) and the break points remain consistently about 1cm off the right edge of the window.
Email Gateway (Aug 19 2022 at 10:46):From: David Greenaway <david.greenaway@nicta.com.au>
On 14/03/13 00:52, Makarius wrote:
On Wed, 13 Mar 2013, John Wickerson wrote:
The word wrapping in the Output window of Isabelle/jEdit is a little
bit off. That is, each line of text breaks about 1cm beyond the
right-hand edge of the Output window (and that's independent of how
I resize the window). Of course it's only a minor quibble because
I can always scroll horizontally a little bit to see the rest of the
output. It doesn't help to turn on/off the gutter.
I also hit this problem, and had a go at fixing, with only minor
success.
I think you mean the breaking of pretty-printed formal output.
(Word-wrap in the source is a different issue: there is also a snag
here, because Isabelle tokenization for {* ... *} is in conflict with
jEdit tokenization for words.)The font metrics and window size parameters for pretty printed output
are only precise once the inner GUI component geometry is known. It
does not quite work with extra decoration (scrollbars, window
borders): before the window is mapped these sizes are unknown, or
I did not know how to get them in Java/AWT/Swing.
I found that "getPainter.getWidth" gave a better indication of a window
size as opposed to getting the control's width and attempting to
subtract off the size of scrollbars, etc.
Another snag I hit is that "metrics.stringWidth" doesn't take into
account anti-aliasing, which after 80 characters of rendering really
starts to add up.
Attached is a patch that may be a starting point to address some of the
problems, but is by no means complete. I still get overflows when
Isabelle renders many wide characters on a line.
I suspect a "proper" solution is to give the line-breaking algorithm
a better understanding of how wide each character is, but I haven't had
a chance to sit down and work out how hard this would be to implement.
Cheers,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
jedit_proof.patch
Email Gateway (Aug 19 2022 at 10:46):From: David Greenaway <david.greenaway@nicta.com.au>
On 14/03/13 10:00, David Greenaway wrote:
I also hit this problem, and had a go at fixing, with only minor
success.
[...]
Attached is a patch that may be a starting point to address some of
the problems, but is by no means complete. I still get overflows when
Isabelle renders many wide characters on a line.I suspect a "proper" solution is to give the line-breaking algorithm
a better understanding of how wide each character is, but I haven't
had a chance to sit down and work out how hard this would be to
implement.
I decided to sit down and actually see if I could come up with a better
solution for this problem. Attached is what I came up with (replacing
my previously posted patch completely).
In particular, "Pretty" internally uses "number of spaces" as its
measuring units. This patch attempts modifies "PrettyTextArea" to more
accurately measure strings and feed these widths into "Pretty" in the
correct units.
This seems to give good results on Linux, with all combinations of
hinted/non-hinted aliased/anti-aliased fixed-width/non-fixed-width fonts
I tried.
A one-space margin remains on the right-hand-side because non-hinted
The patch doesn't attempt to fix SideKick or tool-tips; if the Isabelle
maintainers are happy with the approach in this patch, I would be happy
to extend it.
Cheers,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
jedit_rendering.patch
Last updated: Apr 23 2024 at 20:15 UTC