# HG changeset patch # User wenzelm # Date 1420490832 -3600 # Node ID 569a8109eeb2f7579188fed7db6c46160198ceca # Parent 42710fe5f05a2d4af6ed58104c6abe9242899dad separate module Metrics; maintain static metrics (with font) and visible_graph via layout; diff -r 42710fe5f05a -r 569a8109eeb2 src/Pure/build-jars --- a/src/Pure/build-jars Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Pure/build-jars Mon Jan 05 21:47:12 2015 +0100 @@ -106,6 +106,7 @@ "../Tools/Graphview/graph_panel.scala" "../Tools/Graphview/layout.scala" "../Tools/Graphview/main_panel.scala" + "../Tools/Graphview/metrics.scala" "../Tools/Graphview/model.scala" "../Tools/Graphview/mutator_dialog.scala" "../Tools/Graphview/mutator_event.scala" diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Mon Jan 05 21:47:12 2015 +0100 @@ -12,7 +12,6 @@ import java.awt.{Dimension, Graphics2D, Point} import java.awt.geom.{AffineTransform, Point2D} -import java.awt.image.BufferedImage import javax.swing.{JScrollPane, JComponent, SwingUtilities} import scala.swing.{Panel, ScrollPane} @@ -46,11 +45,8 @@ peer.getVerticalScrollBar.setUnitIncrement(10) def find_visible_node(at: Point2D): Option[Graph_Display.Node] = - { - val m = visualizer.metrics() - visualizer.model.make_visible_graph().keys_iterator - .find(node => visualizer.Drawer.shape(m, node).contains(at)) - } + visualizer.visible_graph.keys_iterator.find(node => + visualizer.Drawer.shape(node).contains(at)) def refresh() { @@ -133,7 +129,7 @@ def scale_discrete: Double = { - val font_height = GUI.line_metrics(visualizer.font()).getHeight.toInt + val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt (scale * font_height).floor / font_height } @@ -147,7 +143,7 @@ def fit_to_window() { - if (visualizer.model.make_visible_graph().is_empty) + if (visualizer.visible_graph.is_empty) rescale(1.0) else { val box = visualizer.Coordinates.bounding_box() @@ -181,18 +177,16 @@ def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] = { - val m = visualizer.metrics() - visualizer.model.make_visible_graph().edges_iterator.map( - edge => - visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find( - { - case (_, (p, _)) => - visualizer.Drawer.shape(m, Graph_Display.Node.dummy). - contains(at.getX() - p.x, at.getY() - p.y) - }) match { - case None => None - case Some((edge, (_, index))) => Some((edge, index)) - } + visualizer.visible_graph.edges_iterator.map(edge => + visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find( + { + case (_, (p, _)) => + visualizer.Drawer.shape(Graph_Display.Node.dummy). + contains(at.getX() - p.x, at.getY() - p.y) + }) match { + case None => None + case Some((edge, (_, index))) => Some((edge, index)) + } } def pressed(at: Point) diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/Graphview/layout.scala Mon Jan 05 21:47:12 2015 +0100 @@ -27,12 +27,13 @@ private type Level = List[Key] private type Levels = List[Level] - val empty = new Layout(Map.empty, Map.empty) + val empty: Layout = + new Layout(Metrics.default, Graph_Display.empty_graph, Map.empty, Map.empty) val pendulum_iterations = 10 val minimize_crossings_iterations = 40 - def make(metrics: Visualizer.Metrics, visible_graph: Graph_Display.Graph): Layout = + def make(metrics: Metrics, visible_graph: Graph_Display.Graph): Layout = { if (visible_graph.is_empty) empty else { @@ -69,7 +70,7 @@ case (map, key) => map + (key -> dummies(key).map(coords(_))) } - new Layout(coords, dummy_coords) + new Layout(metrics, visible_graph, coords, dummy_coords) } } @@ -170,7 +171,7 @@ } def pendulum( - metrics: Visualizer.Metrics, graph: Graph_Display.Graph, + metrics: Metrics, graph: Graph_Display.Graph, levels: Levels, coords: Map[Key, Point]): Coordinates = { type Regions = List[List[Region]] @@ -252,7 +253,7 @@ { var nodes: List[Key] = List(node) - def distance(metrics: Visualizer.Metrics, coords: Coordinates, that: Region): Double = + def distance(metrics: Metrics, coords: Coordinates, that: Region): Double = { val n1 = this.nodes.last; val x1 = coords(n1).x + metrics.box_width2(n1) val n2 = that.nodes.head; val x2 = coords(n2).x - metrics.box_width2(n2) @@ -278,26 +279,36 @@ } final class Layout private( + val metrics: Metrics, + val visible_graph: Graph_Display.Graph, nodes: Map[Graph_Display.Node, Layout.Point], dummies: Map[Graph_Display.Edge, List[Layout.Point]]) { + /* nodes */ + def get_node(node: Graph_Display.Node): Layout.Point = nodes.getOrElse(node, Layout.Point.zero) def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout = nodes.get(node) match { case None => this - case Some(p) => new Layout(nodes + (node -> f(p)), dummies) + case Some(p) => + val nodes1 = nodes + (node -> f(p)) + new Layout(metrics, visible_graph, nodes1, dummies) } + /* dummies */ + def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = dummies.getOrElse(edge, Nil) def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout = dummies.get(edge) match { case None => this - case Some(ds) => new Layout(nodes, dummies + (edge -> f(ds))) + case Some(ds) => + val dummies1 = dummies + (edge -> f(ds)) + new Layout(metrics, visible_graph, nodes, dummies1) } } diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/metrics.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/metrics.scala Mon Jan 05 21:47:12 2015 +0100 @@ -0,0 +1,45 @@ +/* Title: Tools/Graphview/metrics.scala + Author: Makarius + +Physical metrics for layout and painting. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.{Font, RenderingHints} +import java.awt.font.FontRenderContext + + +object Metrics +{ + val rendering_hints: RenderingHints = + new RenderingHints(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON) + + val font_render_context: FontRenderContext = + new FontRenderContext(null, true, false) + + def apply(font: Font): Metrics = new Metrics(font) + + val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) +} + +class Metrics private(val font: Font) +{ + def string_bounds(s: String) = font.getStringBounds(s, Metrics.font_render_context) + private val mix = string_bounds("mix") + val space_width = string_bounds(" ").getWidth + def char_width: Double = mix.getWidth / 3 + def height: Double = mix.getHeight + def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent + def gap: Double = mix.getWidth + def pad: Double = char_width + + def box_width2(node: Graph_Display.Node): Double = + ((string_bounds(node.toString).getWidth + pad) / 2).ceil + def box_gap: Double = gap.ceil + def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil +} + diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/Graphview/popups.scala Mon Jan 05 21:47:12 2015 +0100 @@ -24,7 +24,7 @@ val visualizer = panel.visualizer val add_mutator = visualizer.model.Mutators.add _ - val visible_graph = visualizer.model.make_visible_graph() + val visible_graph = visualizer.visible_graph def filter_context( nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) = diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/Graphview/shapes.scala Mon Jan 05 21:47:12 2015 +0100 @@ -21,22 +21,22 @@ object Node { - def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node) - : Rectangle2D.Double = + def shape(visualizer: Visualizer, node: Graph_Display.Node): Rectangle2D.Double = { + val metrics = visualizer.metrics val p = visualizer.Coordinates.get_node(node) - val bounds = m.string_bounds(node.toString) - val w = bounds.getWidth + m.pad - val h = bounds.getHeight + m.pad + val bounds = metrics.string_bounds(node.toString) + val w = bounds.getWidth + metrics.pad + val h = bounds.getHeight + metrics.pad new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil) } def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) { - val m = Visualizer.Metrics(gfx) - val s = shape(m, visualizer, node) + val metrics = visualizer.metrics + val s = shape(visualizer, node) val c = visualizer.node_color(node) - val bounds = m.string_bounds(node.toString) + val bounds = metrics.string_bounds(node.toString) gfx.setColor(c.background) gfx.fill(s) @@ -46,9 +46,10 @@ gfx.draw(s) gfx.setColor(c.foreground) + gfx.setFont(metrics.font) gfx.drawString(node.toString, (s.getCenterX - bounds.getWidth / 2).round.toInt, - (s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt) + (s.getCenterY - bounds.getHeight / 2 + metrics.ascent).round.toInt) } } @@ -56,8 +57,9 @@ { private val identity = new AffineTransform() - def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape = + def shape(visualizer: Visualizer): Shape = { + val m = visualizer.metrics val w = (m.space_width / 2).ceil new Rectangle2D.Double(- w, - w, 2 * w, 2 * w) } @@ -67,12 +69,9 @@ def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform) { - val m = Visualizer.Metrics(gfx) - val s = shape(m, visualizer) - gfx.setStroke(default_stroke) gfx.setColor(visualizer.dummy_color) - gfx.draw(at.createTransformedShape(s)) + gfx.draw(at.createTransformedShape(shape(visualizer))) } } @@ -103,9 +102,7 @@ gfx.setColor(visualizer.edge_color(edge)) gfx.draw(path) - if (head) - Arrow_Head.paint(gfx, path, - visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2)) + if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2)) } } @@ -160,9 +157,7 @@ gfx.setColor(visualizer.edge_color(edge)) gfx.draw(path) - if (head) - Arrow_Head.paint(gfx, path, - visualizer.Drawer.shape(Visualizer.Metrics(gfx), edge._2)) + if (head) Arrow_Head.paint(gfx, path, visualizer.Drawer.shape(edge._2)) } } } diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/Graphview/visualizer.scala --- a/src/Tools/Graphview/visualizer.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/Graphview/visualizer.scala Mon Jan 05 21:47:12 2015 +0100 @@ -10,46 +10,21 @@ import isabelle._ -import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D} -import java.awt.font.FontRenderContext -import java.awt.image.BufferedImage +import java.awt.{Font, Color, Shape, Graphics2D} import java.awt.geom.Rectangle2D import javax.swing.JComponent -object Visualizer -{ - object Metrics - { - def apply(font: Font, font_render_context: FontRenderContext) = - new Metrics(font, font_render_context) - - def apply(gfx: Graphics2D): Metrics = - new Metrics(gfx.getFont, gfx.getFontRenderContext) - } - - class Metrics private(font: Font, font_render_context: FontRenderContext) - { - def string_bounds(s: String) = font.getStringBounds(s, font_render_context) - private val mix = string_bounds("mix") - val space_width = string_bounds(" ").getWidth - def char_width: Double = mix.getWidth / 3 - def height: Double = mix.getHeight - def ascent: Double = font.getLineMetrics("", font_render_context).getAscent - def gap: Double = mix.getWidth - def pad: Double = char_width - - def box_width2(node: Graph_Display.Node): Double = - ((string_bounds(node.toString).getWidth + pad) / 2).ceil - def box_gap: Double = gap.ceil - def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil - } -} - class Visualizer(options: => Options, val model: Model) { visualizer => + // owned by GUI thread + private var layout: Layout = Layout.empty + + def metrics: Metrics = layout.metrics + def visible_graph: Graph_Display.Graph = layout.visible_graph + /* tooltips */ @@ -67,23 +42,13 @@ /* font rendering information */ - def font(): Font = + def make_font(): Font = { val family = options.string("graphview_font_family") val size = options.int("graphview_font_size") new Font(family, Font.PLAIN, size) } - val rendering_hints = - new RenderingHints( - RenderingHints.KEY_ANTIALIASING, - RenderingHints.VALUE_ANTIALIAS_ON) - - val font_render_context = new FontRenderContext(null, true, false) - - def metrics(): Visualizer.Metrics = - Visualizer.Metrics(font(), font_render_context) - /* rendering parameters */ @@ -112,9 +77,6 @@ object Coordinates { - // owned by GUI thread - private var layout = Layout.empty - def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node) def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge) @@ -137,28 +99,31 @@ def update_layout() { + val metrics = Metrics(make_font()) + val visible_graph = model.make_visible_graph() + // FIXME avoid expensive operation on GUI thread - layout = Layout.make(metrics(), model.make_visible_graph()) + layout = Layout.make(metrics, visible_graph) } def bounding_box(): Rectangle2D.Double = { - val m = metrics() var x0 = 0.0 var y0 = 0.0 var x1 = 0.0 var y1 = 0.0 - for (node <- model.make_visible_graph().keys_iterator) { - val shape = Shapes.Node.shape(m, visualizer, node) + for (node <- visible_graph.keys_iterator) { + val shape = Shapes.Node.shape(visualizer, node) x0 = x0 min shape.getMinX y0 = y0 min shape.getMinY x1 = x1 max shape.getMaxX y1 = y1 max shape.getMaxY } - x0 = (x0 - m.gap).floor - y0 = (y0 - m.gap).floor - x1 = (x1 + m.gap).ceil - y1 = (y1 + m.gap).ceil + val gap = metrics.gap + x0 = (x0 - gap).floor + y0 = (y0 - gap).floor + x1 = (x1 + gap).ceil + y1 = (y1 + gap).ceil new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) } } @@ -173,16 +138,14 @@ def paint_all_visible(gfx: Graphics2D, dummies: Boolean) { - gfx.setFont(font()) - gfx.setRenderingHints(rendering_hints) - val visible_graph = model.make_visible_graph() + gfx.setRenderingHints(Metrics.rendering_hints) visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies)) visible_graph.keys_iterator.foreach(apply(gfx, _)) } - def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape = - if (node.is_dummy) Shapes.Dummy.shape(m, visualizer) - else Shapes.Node.shape(m, visualizer, node) + def shape(node: Graph_Display.Node): Shape = + if (node.is_dummy) Shapes.Dummy.shape(visualizer) + else Shapes.Node.shape(visualizer, node) } object Selection diff -r 42710fe5f05a -r 569a8109eeb2 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 21:47:12 2015 +0100 @@ -78,7 +78,7 @@ override def selection_color = view.getTextArea.getPainter.getSelectionColor override def error_color = PIDE.options.color_value("error_color") - override def font() = + override def make_font(): Font = GUI.imitate_font(Font_Info.main().font, PIDE.options.string("graphview_font_family"), PIDE.options.real("graphview_font_scale"))