merged
authorwenzelm
Sat, 23 Mar 2013 21:19:10 +0100
changeset 51499 e7f80c4f8238
parent 51490 7edcc0618dae (current diff)
parent 51498 979592b765f8 (diff)
child 51500 01fe31f05aa8
merged
--- a/src/Pure/General/pretty.ML	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Pure/General/pretty.ML	Sat Mar 23 21:19:10 2013 +0100
@@ -79,12 +79,13 @@
 (** spaces **)
 
 local
-  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
+  val small_spaces = Vector.tabulate (65, fn i => replicate_string i Symbol.space);
 in
   fun spaces k =
     if k < 64 then Vector.sub (small_spaces, k)
-    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
-      Vector.sub (small_spaces, k mod 64);
+    else
+      replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
+        Vector.sub (small_spaces, k mod 64);
 end;
 
 
--- a/src/Pure/General/pretty.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Pure/General/pretty.scala	Sat Mar 23 21:19:10 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)
@@ -72,30 +89,16 @@
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
-  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
+  private val margin_default = 76.0
 
-  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 =
+  def formatted(input: XML.Body, margin: Double = margin_default,
+    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 =
+  def string_of(input: XML.Body, margin: Double = margin_default,
+      metric: Metric = Metric_Default): String =
     XML.content(formatted(input, margin, metric))
 
 
--- a/src/Pure/PIDE/command.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -21,17 +21,19 @@
 
   object Results
   {
+    type Entry = (Long, XML.Tree)
     val empty = new Results(SortedMap.empty)
+    def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
     def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
   }
 
-  final class Results private(rep: SortedMap[Long, XML.Tree])
+  final class Results private(private val rep: SortedMap[Long, XML.Tree])
   {
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Tree] = rep.get(serial)
-    def entries: Iterator[(Long, XML.Tree)] = rep.iterator
+    def entries: Iterator[Results.Entry] = rep.iterator
 
-    def + (entry: (Long, XML.Tree)): Results =
+    def + (entry: Results.Entry): Results =
       if (defined(entry._1)) this
       else new Results(rep + entry)
 
@@ -40,6 +42,12 @@
       else if (rep.isEmpty) other
       else (this /: other.entries)(_ + _)
 
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Results => rep == other.rep
+        case _ => false
+      }
     override def toString: String = entries.mkString("Results(", ", ", ")")
   }
 
@@ -56,7 +64,13 @@
       markup.to_XML(command.range, command.source, filter)
 
 
-    /* accumulate content */
+    /* content */
+
+    def eq_content(other: State): Boolean =
+      command.source == other.command.source &&
+      status == other.status &&
+      results == other.results &&
+      markup == other.markup
 
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
--- a/src/Pure/PIDE/document.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -277,7 +277,7 @@
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
-    def eq_markup(other: Snapshot): Boolean
+    def eq_content(other: Snapshot): Boolean
     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
       result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
@@ -494,14 +494,13 @@
         def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
         def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
 
-        def eq_markup(other: Snapshot): Boolean =
+        def eq_content(other: Snapshot): Boolean =
           !is_outdated && !other.is_outdated &&
             node.commands.size == other.node.commands.size &&
             ((node.commands.iterator zip other.node.commands.iterator) forall {
               case (cmd1, cmd2) =>
-                cmd1.source == cmd2.source &&
-                (state.command_state(version, cmd1).markup eq
-                 other.state.command_state(other.version, cmd2).markup)
+                state.command_state(version, cmd1) eq_content
+                  other.state.command_state(other.version, cmd2)
             })
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -65,7 +65,8 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             val rendering = Rendering(snapshot, PIDE.options.value)
-            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
+            Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty,
+              Text.Range(-1), body)
             null
           }
         }
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -201,7 +201,8 @@
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
                 val info_text =
-                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
+                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
+                    .mkString
 
                 new DefaultMutableTreeNode(
                   new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Mar 23 21:19:10 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 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -21,14 +21,6 @@
 
 object Pretty_Text_Area
 {
-  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
-    formatted_body: XML.Body): (String, Rendering) =
-  {
-    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, base_results, formatted_body)
-    val rendering = Rendering(state.snapshot(), PIDE.options.value)
-    (text, rendering)
-  }
-
   private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
     formatted_body: XML.Body): (String, Document.State) =
   {
@@ -50,6 +42,14 @@
 
     (command.source, state1)
   }
+
+  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
+    formatted_body: XML.Body): (String, Rendering) =
+  {
+    val (text, state) = document_state(base_snapshot, base_results, formatted_body)
+    val rendering = Rendering(state.snapshot(), PIDE.options.value)
+    (text, rendering)
+  }
 }
 
 class Pretty_Text_Area(
@@ -83,6 +83,7 @@
     val font = new Font(current_font_family, Font.PLAIN, current_font_size)
     getPainter.setFont(font)
     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
+    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
 
     val fold_line_style = new Array[SyntaxStyle](4)
@@ -108,12 +109,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) max 20.0
 
       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 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -39,6 +39,7 @@
     rendering: Rendering,
     mouse_x: Int, mouse_y: Int,
     results: Command.Results,
+    range: Text.Range,
     body: XML.Body): Pretty_Tooltip =
   {
     Swing_Thread.require()
@@ -63,7 +64,7 @@
           others.foreach(_.dispose)
           window
       }
-    window.init(rendering, parent, mouse_x, mouse_y, results, body)
+    window.init(rendering, parent, mouse_x, mouse_y, results, range, body)
     window
   }
 
@@ -104,6 +105,7 @@
   private var current_rendering: Rendering =
     Rendering(Document.State.init.snapshot(), PIDE.options.value)
   private var current_results = Command.Results.empty
+  private var current_range = Text.Range(-1)
   private var current_body: XML.Body = Nil
 
 
@@ -168,60 +170,64 @@
     parent: JComponent,
     mouse_x: Int, mouse_y: Int,
     results: Command.Results,
+    range: Text.Range,
     body: XML.Body)
   {
-    current_rendering = rendering
-    current_results = results
-    current_body = body
+    if (!(results == current_results && range == current_range && body == current_body)) {
+      current_rendering = rendering
+      current_results = results
+      current_range = range
+      current_body = body
 
-    pretty_text_area.resize(Rendering.font_family(),
-      Rendering.font_size("jedit_tooltip_font_scale").round)
-    pretty_text_area.update(rendering.snapshot, results, body)
+      pretty_text_area.resize(Rendering.font_family(),
+        Rendering.font_size("jedit_tooltip_font_scale").round)
+      pretty_text_area.update(rendering.snapshot, results, body)
 
-    content_panel.setBackground(rendering.tooltip_color)
-    controls.background = rendering.tooltip_color
+      content_panel.setBackground(rendering.tooltip_color)
+      controls.background = rendering.tooltip_color
 
 
-    /* window geometry */
+      /* window geometry */
+
+      val screen_point = new Point(mouse_x, mouse_y)
+      SwingUtilities.convertPointToScreen(screen_point, parent)
+      val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
 
-    val screen_point = new Point(mouse_x, mouse_y)
-    SwingUtilities.convertPointToScreen(screen_point, parent)
-    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
+      {
+        val painter = pretty_text_area.getPainter
+        val metric = JEdit_Lib.pretty_metric(painter)
+        val margin = rendering.tooltip_margin * metric.average
+        val lines =
+          XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
+            (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
-    {
-      val painter = pretty_text_area.getPainter
-      val fm = painter.getFontMetrics
-      val margin = rendering.tooltip_margin
-      val lines =
-        XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
-          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+        if (window.getWidth == 0) {
+          window.setSize(new Dimension(100, 100))
+          window.setPreferredSize(new Dimension(100, 100))
+        }
+        window.pack
+        window.revalidate
+
+        val deco_width = window.getWidth - painter.getWidth
+        val deco_height = window.getHeight - painter.getHeight
 
-      if (window.getWidth == 0) {
-        window.setSize(new Dimension(100, 100))
-        window.setPreferredSize(new Dimension(100, 100))
+        val bounds = rendering.tooltip_bounds
+        val w =
+          ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
+          (screen_bounds.width * bounds).toInt
+        val h =
+          (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min
+          (screen_bounds.height * bounds).toInt
+
+        window.setSize(new Dimension(w, h))
+        window.setPreferredSize(new Dimension(w, h))
+        window.pack
+        window.revalidate
+
+        val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
+        val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
+        window.setLocation(x, y)
       }
-      window.pack
-      window.revalidate
-
-      val deco_width = window.getWidth - painter.getWidth
-      val deco_height = window.getHeight - painter.getHeight
-
-      val bounds = rendering.tooltip_bounds
-      val w =
-        ((Pretty.char_width(fm) * (margin + 1)).round.toInt + deco_width) min
-        (screen_bounds.width * bounds).toInt
-      val h =
-        (fm.getHeight * (lines + 1) + deco_height) min
-        (screen_bounds.height * bounds).toInt
-
-      window.setSize(new Dimension(w, h))
-      window.setPreferredSize(new Dimension(w, h))
-      window.pack
-      window.revalidate
-
-      val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
-      val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
-      window.setLocation(x, y)
     }
 
     window.setVisible(true)
--- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -275,22 +275,30 @@
     (Command.Results.empty /: results)(_ ++ _)
   }
 
-  def tooltip_message(range: Text.Range): XML.Body =
+  def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
-    val msgs =
-      Command.Results.merge(
-        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
-          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
-          {
-            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
-            if name == Markup.WRITELN ||
-                name == Markup.WARNING ||
-                name == Markup.ERROR =>
-              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
-            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
-            if !body.isEmpty => msgs + (Document.new_id() -> msg)
-          }).map(_.info))
-    Pretty.separate(msgs.entries.map(_._2).toList)
+    val results =
+      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
+        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+        {
+          case (msgs, Text.Info(info_range,
+            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+          if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
+            val entry: Command.Results.Entry =
+              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+            Text.Info(snapshot.convert(info_range), entry) :: msgs
+
+          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+          if !body.isEmpty =>
+            val entry: Command.Results.Entry = (Document.new_id(), msg)
+            Text.Info(snapshot.convert(info_range), entry) :: msgs
+        }).toList.flatMap(_.info)
+    if (results.isEmpty) None
+    else {
+      val r = Text.Range(results.head.range.start, results.last.range.stop)
+      val msgs = Command.Results.make(results.map(_.info))
+      Some(Text.Info(r, Pretty.separate(msgs.entries.map(_._2).toList)))
+    }
   }
 
 
@@ -317,12 +325,15 @@
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
 
-  def tooltip(range: Text.Range): XML.Body =
+  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
-    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
+    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
+    {
+      val r = snapshot.convert(r0)
       if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
+    }
 
-    val tips =
+    val results =
       snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
         range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
         {
@@ -340,11 +351,15 @@
             add(prev, r, (false, pretty_typing("ML:", body)))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
           if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
-        }).toList.flatMap(_.info.info)
+        }).toList.map(_.info)
 
-    val all_tips =
-      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
-    Library.separate(Pretty.FBreak, all_tips.toList)
+    results.flatMap(_.info) match {
+      case Nil => None
+      case tips =>
+        val r = Text.Range(results.head.range.start, results.last.range.stop)
+        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
+        Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
+    }
   }
 
   val tooltip_margin: Int = options.int("jedit_tooltip_margin")
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -215,14 +215,16 @@
             JEdit_Lib.pixel_range(text_area, x, y) match {
               case None =>
               case Some(range) =>
-                val tip =
+                val result =
                   if (control) rendering.tooltip(range)
                   else rendering.tooltip_message(range)
-                if (!tip.isEmpty) {
-                  val painter = text_area.getPainter
-                  val y1 = y + painter.getFontMetrics.getHeight / 2
-                  val results = rendering.command_results(range)
-                  Pretty_Tooltip(view, painter, rendering, x, y1, results, tip)
+                result match {
+                  case None =>
+                  case Some(tip) =>
+                    val painter = text_area.getPainter
+                    val y1 = y + painter.getFontMetrics.getHeight / 2
+                    val results = rendering.command_results(range)
+                    Pretty_Tooltip(view, painter, rendering, x, y1, results, tip.range, tip.info)
                 }
             }
           }
@@ -497,11 +499,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)
           }
         }
       }
--- a/src/Tools/jEdit/src/text_overview.scala	Sat Mar 23 20:57:57 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Sat Mar 23 21:19:10 2013 +0100
@@ -101,7 +101,7 @@
 
           if (!(line_count == last_line_count && char_count == last_char_count &&
                 L == last_L && H == last_H && relevant_range == last_relevant_range &&
-                (snapshot eq_markup last_snapshot) && (options eq last_options)))
+                (snapshot eq_content last_snapshot) && (options eq last_options)))
           {
             @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
               : List[(Color, Int, Int)] =