# HG changeset patch # User wenzelm # Date 1364069950 -3600 # Node ID e7f80c4f8238b87e9ab660a48291d7028d2ec5fa # Parent 7edcc0618dae2a282760253c9660e4f882459c04# Parent 979592b765f85cedf8e182a56271634b5b52166c merged diff -r 7edcc0618dae -r e7f80c4f8238 src/Pure/General/pretty.ML --- 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; diff -r 7edcc0618dae -r e7f80c4f8238 src/Pure/General/pretty.scala --- 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)) diff -r 7edcc0618dae -r e7f80c4f8238 src/Pure/PIDE/command.scala --- 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) diff -r 7edcc0618dae -r e7f80c4f8238 src/Pure/PIDE/document.scala --- 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]], diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/graphview_dockable.scala --- 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 } } diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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) { diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/jedit_lib.scala --- 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 + } } diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/pretty_text_area.scala --- 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(() => diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/rendering.scala --- 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") diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/rich_text_area.scala --- 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) } } } diff -r 7edcc0618dae -r e7f80c4f8238 src/Tools/jEdit/src/text_overview.scala --- 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)] =