--- 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)] =