src/Pure/General/pretty.scala | 20 +++++++++----------- src/Tools/jEdit/src/jedit_lib.scala | 6 +++--- src/Tools/jEdit/src/pretty_text_area.scala | 2 +- src/Tools/jEdit/src/pretty_tooltip.scala | 2 +- src/Tools/jEdit/src/rich_text_area.scala | 2 +- 5 files changed, 15 insertions(+), 17 deletions(-)
________________________________ 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.
# HG changeset patch # User David Greenaway <[email protected]> # Date 1363843205 -39600 # Node ID b1420574b7273225672a9f7e6a5b3e9c6c84b75d # Parent e0c74b23d0a87547465aced2020de1998175662a pretty: Ensure we are consistent in our use of space-widths versus character-widths. The current version of "pretty.scala" internally uses spaces to pad out indented lines. Unfortunately, it internally measures the width of these strings of spaces using "char_width", which is an approximation of the average width of characters in the current font. This is particularly noticeable in jEdit when using a font where the width of a space character is a significantly different width from other characters. We replace "char_width" and "char_width_int" with a new method "space_width", and adjust callers to use these new methods instead. diff --git a/src/Pure/General/pretty.scala b/src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala +++ b/src/Pure/General/pretty.scala @@ -163,14 +163,13 @@ /** Default implementation for measuring a string. */ private def metric_default(s: String) = s.length.toDouble - /** Returns an approximation of the width of an average character in the - * given [[FontMetrics]], measured in pixels. */ - def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3 - def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt + /** Returns the width of a single space character in the given [[FontMetrics]], + * measured in pixels. */ + def space_width(metrics: FontMetrics): Int = metrics.stringWidth(" ") max 1 - /** Returns the width of the given string. + /** Returns the width of the given string, in spaces. * - * The unit returned is "average character widths". For example: + * For example: * * {{{ * font_metic(font, "isabelle") @@ -180,11 +179,10 @@ * in. */ def font_metric(metrics: FontMetrics): String => Double = - if (metrics == null) ((s: String) => s.length.toDouble) - else { - val unit = char_width(metrics) - ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit) - } + { + val unit = space_width(metrics) + ((s: String) => metrics.stringWidth(s) / unit) + } /** Annotates the given [[XML.Body]] containing indentation and line breaking * information with concrete formatting directives so that it can be printed diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala +++ b/src/Tools/jEdit/src/jedit_lib.scala @@ -168,7 +168,7 @@ // NB: last line lacks \n def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { - val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics) + val space_width = Pretty.space_width(text_area.getPainter.getFontMetrics) val buffer = text_area.getBuffer @@ -179,9 +179,9 @@ try { val p = text_area.offsetToXY(range.start) val (q, r) = - if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) + if (stop >= end) (text_area.offsetToXY(end), space_width * (stop - end)) else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") - (text_area.offsetToXY(stop - 1), char_width) + (text_area.offsetToXY(stop - 1), space_width) else (text_area.offsetToXY(stop), 0) (p, q, r) } diff --git a/src/Tools/jEdit/src/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala +++ b/src/Tools/jEdit/src/pretty_text_area.scala @@ -109,7 +109,7 @@ if (getWidth > 0) { val fm = getPainter.getFontMetrics - val margin = (getPainter.getWidth / (Pretty.char_width_int(fm) max 1)) max 20 + val margin = (getPainter.getWidth / Pretty.space_width(fm)) max 20 val base_snapshot = current_base_snapshot val base_results = current_base_results diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala +++ b/src/Tools/jEdit/src/pretty_tooltip.scala @@ -208,7 +208,7 @@ val bounds = rendering.tooltip_bounds val w = - ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min + ((Pretty.space_width(fm) * (margin + 1)) + deco_width) min (screen_bounds.width * bounds).toInt val h = (fm.getHeight * (lines + 1) + deco_height) min diff --git a/src/Tools/jEdit/src/rich_text_area.scala b/src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala +++ b/src/Tools/jEdit/src/rich_text_area.scala @@ -501,7 +501,7 @@ val offset = caret - text_area.getLineStartOffset(physical_line) val x = text_area.offsetToXY(physical_line, offset).x gfx.setColor(painter.getCaretColor) - gfx.drawRect(x, y, Pretty.char_width_int(fm) - 1, fm.getHeight - 1) + gfx.drawRect(x, y, Pretty.space_width(fm) - 1, fm.getHeight - 1) } } }
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
