more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
--- a/src/Pure/General/pretty.scala Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Pure/General/pretty.scala Sat Mar 23 13:12:39 2013 +0100
@@ -26,6 +26,23 @@
}
+ /* text metric -- standardized to width of space */
+
+ abstract class Metric
+ {
+ val unit: Double
+ def average: Double
+ def apply(s: String): Double
+ }
+
+ object Metric_Default extends Metric
+ {
+ val unit = 1.0
+ val average = 1.0
+ def apply(s: String): Double = s.length.toDouble
+ }
+
+
/* markup trees with physical blocks and breaks */
def block(body: XML.Body): XML.Tree = Block(2, body)
@@ -73,29 +90,15 @@
}
private val margin_default = 76
- private def metric_default(s: String) = s.length.toDouble
-
- def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3
-
- 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)
- }
def formatted(input: XML.Body, margin: Int = margin_default,
- metric: String => Double = metric_default): XML.Body =
+ metric: Metric = Metric_Default): XML.Body =
{
sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
{
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
- def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
- def blanks(wd: Int): Text =
- {
- val s = spaces(wd)
- string(s, metric(s))
- }
+ def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
+ def blanks(wd: Int): Text = string(spaces(wd))
def content: XML.Body = tx.reverse
}
@@ -153,14 +156,14 @@
val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
- case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
+ case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
}
format(standard_format(input), 0.0, 0.0, Text()).content
}
def string_of(input: XML.Body, margin: Int = margin_default,
- metric: String => Double = metric_default): String =
+ metric: Metric = Metric_Default): String =
XML.content(formatted(input, margin, metric))
--- a/src/Tools/jEdit/src/jedit_lib.scala Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Mar 23 13:12:39 2013 +0100
@@ -15,7 +15,7 @@
import org.gjt.sp.jedit.{jEdit, Buffer, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
object JEdit_Lib
@@ -168,7 +168,8 @@
// NB: last line lacks \n
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
{
- val char_width = Pretty.char_width(text_area.getPainter.getFontMetrics).round.toInt
+ val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
+ val char_width = (metric.unit * metric.average).round.toInt
val buffer = text_area.getBuffer
@@ -203,5 +204,18 @@
case _ => None
}
}
+
+
+ /* pretty text metric */
+
+ def string_width(painter: TextAreaPainter, s: String): Double =
+ painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+
+ def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
+ new Pretty.Metric {
+ val unit = string_width(painter, Pretty.space)
+ val average = string_width(painter, "mix") / (3 * unit)
+ def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit
+ }
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 23 13:12:39 2013 +0100
@@ -108,12 +108,12 @@
getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
if (getWidth > 0) {
- val fm = getPainter.getFontMetrics
- val margin = (getPainter.getWidth / (Pretty.char_width(fm).ceil.toInt max 1)) max 20
+ val metric = JEdit_Lib.pretty_metric(getPainter)
+ val margin = (getPainter.getWidth.toDouble / metric.unit).toInt max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
- val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(fm))
+ val formatted_body = Pretty.formatted(current_body, margin, metric)
future_rendering.map(_.cancel(true))
future_rendering = Some(default_thread_pool.submit(() =>
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Mar 23 13:12:39 2013 +0100
@@ -190,10 +190,10 @@
{
val painter = pretty_text_area.getPainter
- val fm = painter.getFontMetrics
- val margin = rendering.tooltip_margin
+ val metric = JEdit_Lib.pretty_metric(painter)
+ val margin = (rendering.tooltip_margin * metric.average).toInt
val lines =
- XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
+ XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
if (window.getWidth == 0) {
@@ -208,10 +208,10 @@
val bounds = rendering.tooltip_bounds
val w =
- ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
+ ((metric.unit * (margin + 1)).round.toInt + deco_width) min
(screen_bounds.width * bounds).toInt
val h =
- (fm.getHeight * (lines + 1) + deco_height) min
+ (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
(screen_bounds.height * bounds).toInt
window.setSize(new Dimension(w, h))
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 23 13:04:28 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 23 13:12:39 2013 +0100
@@ -497,11 +497,12 @@
if (start <= caret && caret == end - 1) {
val painter = text_area.getPainter
val fm = painter.getFontMetrics
+ val metric = JEdit_Lib.pretty_metric(painter)
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(fm).round.toInt - 1, fm.getHeight - 1)
+ gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
}
}
}