--- a/src/Pure/GUI/gui.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/GUI/gui.scala Mon Jan 05 23:33:39 2015 +0100
@@ -218,14 +218,14 @@
def line_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
- def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
+ def imitate_font(font: Font, family: String, scale: Double = 1.0): Font =
{
val font1 = new Font(family, font.getStyle, font.getSize)
- val size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight * font.getSize
- font1.deriveFont((scale * size).toInt)
+ val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
+ new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
}
- def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String =
+ def imitate_font_css(font: Font, family: String, scale: Double = 1.0): String =
{
val font1 = new Font(family, font.getStyle, font.getSize)
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
--- a/src/Pure/General/graph_display.ML Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/General/graph_display.ML Mon Jan 05 23:33:39 2015 +0100
@@ -13,8 +13,6 @@
val eq_entry: entry * entry -> bool
val sort_graph: entry list -> entry list
val write_graph_browser: Path.T -> entry list -> unit
- val browserN: string
- val graphviewN: string
val display_graph: entry list -> unit
end;
@@ -60,17 +58,6 @@
in ((#2 key, node), map #2 (Graph.Keys.dest preds)) end));
-(* print modes *)
-
-val browserN = "browser";
-val graphviewN = "graphview";
-
-fun is_browser () =
- (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
- SOME m => m = browserN
- | NONE => true);
-
-
(* encode graph *)
val encode_browser =
@@ -97,11 +84,18 @@
val display_graph =
sort_graph #> (fn entries =>
let
- val (markup, body) =
- if is_browser () then (Markup.browserN, encode_browser entries)
- else (Markup.graphviewN, YXML.string_of_body (encode_graph entries));
+ val ((bg1, bg2), en) =
+ YXML.output_markup_elem
+ (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+ val _ =
+ writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "new graph" ^ en);
+
val ((bg1, bg2), en) =
- YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
- in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end);
+ YXML.output_markup_elem
+ (Active.make_markup Markup.browserN {implicit = false, properties = []});
+ val _ =
+ writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
+ in () end);
+
end;
--- a/src/Pure/build-jars Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Pure/build-jars Mon Jan 05 23:33:39 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/etc/options Mon Jan 05 23:33:39 2015 +0100
@@ -0,0 +1,12 @@
+(* :mode=isabelle-options: *)
+
+section "Graphview"
+
+option graphview_font_family : string = "Helvetica"
+ -- "base font family (notably for PDF)"
+
+option graphview_font_size : int = 12
+ -- "base font size (notably for PDF)"
+
+public option graphview_font_scale : real = 0.85
+ -- "scale factor of graph view wrt. main text font"
--- a/src/Tools/Graphview/graph_panel.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Mon Jan 05 23:33:39 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 =>
+ Shapes.Node.shape(visualizer, node).contains(at))
def refresh()
{
@@ -100,7 +96,7 @@
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
gfx.transform(Transform())
- visualizer.Drawer.paint_all_visible(gfx, true)
+ visualizer.paint_all_visible(gfx)
}
}
private val paint_panel = new Paint_Panel
@@ -132,7 +128,10 @@
}
def scale_discrete: Double =
- (scale * visualizer.font_size).floor / visualizer.font_size
+ {
+ val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt
+ (scale * font_height).floor / font_height
+ }
def apply() =
{
@@ -144,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()
@@ -177,20 +176,12 @@
}
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.
+ collectFirst({
+ case (edge, (d, index))
+ if Shapes.Dummy.shape(visualizer, d).contains(at) => (edge, index)
+ })
def pressed(at: Point)
{
--- a/src/Tools/Graphview/layout.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/layout.scala Mon Jan 05 23:33:39 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,39 @@
}
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)
}
+
+ def dummies_iterator: Iterator[Layout.Point] =
+ for { (_, ds) <- dummies.iterator; d <- ds.iterator } yield d
}
--- a/src/Tools/Graphview/main_panel.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Mon Jan 05 23:33:39 2015 +0100
@@ -13,9 +13,7 @@
import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser}
import java.io.{File => JFile}
-import java.awt.{Color, Dimension, Graphics2D}
-import java.awt.geom.Rectangle2D
-import java.awt.image.BufferedImage
+import java.awt.{Color, Graphics2D}
import javax.imageio.ImageIO
import javax.swing.border.EmptyBorder
import javax.swing.JComponent
@@ -45,6 +43,10 @@
selected = visualizer.arrow_heads
action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
},
+ new CheckBox() {
+ selected = visualizer.show_dummies
+ action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+ },
new Button {
action = Action("Save image") {
chooser.showSaveDialog(this) match {
@@ -72,9 +74,8 @@
{
gfx.setColor(Color.WHITE)
gfx.fillRect(0, 0, w, h)
-
gfx.translate(- box.x, - box.y)
- visualizer.Drawer.paint_all_visible(gfx, false)
+ visualizer.paint_all_visible(gfx)
}
try {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/metrics.scala Mon Jan 05 23:33:39 2015 +0100
@@ -0,0 +1,46 @@
+/* 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_x: Double = char_width * 1.5
+ def pad_y: Double = char_width
+
+ def box_width2(node: Graph_Display.Node): Double =
+ ((string_bounds(node.toString).getWidth + pad_x) / 2).ceil
+ def box_gap: Double = gap.ceil
+ def box_height(n: Int): Double = (char_width * 1.5 * (5 max n)).ceil
+}
+
--- a/src/Tools/Graphview/popups.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/popups.scala Mon Jan 05 23:33:39 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) =
--- a/src/Tools/Graphview/shapes.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Mon Jan 05 23:33:39 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_x
+ val h = bounds.getHeight + metrics.pad_y
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,40 +46,33 @@
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)
}
}
object Dummy
{
- private val identity = new AffineTransform()
-
- def shape(m: Visualizer.Metrics, visualizer: Visualizer): Shape =
+ def shape(visualizer: Visualizer, d: Layout.Point): Rectangle2D.Double =
{
- val w = (m.space_width / 2).ceil
- new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
+ val metrics = visualizer.metrics
+ val w = metrics.pad_x
+ new Rectangle2D.Double((d.x - (w / 2)).floor, (d.y - (w / 2)).floor, w.ceil, w.ceil)
}
- def paint(gfx: Graphics2D, visualizer: Visualizer): Unit =
- paint_transformed(gfx, visualizer, identity)
-
- def paint_transformed(gfx: Graphics2D, visualizer: Visualizer, at: AffineTransform)
+ def paint(gfx: Graphics2D, visualizer: Visualizer, d: Layout.Point)
{
- 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(shape(visualizer, d))
}
}
object Straight_Edge
{
- def paint(gfx: Graphics2D, visualizer: Visualizer,
- edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+ def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
{
val p = visualizer.Coordinates.get_node(edge._1)
val q = visualizer.Coordinates.get_node(edge._2)
@@ -95,17 +88,15 @@
ds.foreach(d => path.lineTo(d.x, d.y))
path.lineTo(q.x, q.y)
- if (dummies)
- ds.foreach(d =>
- Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+ if (visualizer.show_dummies)
+ ds.foreach(Dummy.paint(gfx, visualizer, _))
gfx.setStroke(default_stroke)
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 (visualizer.arrow_heads)
+ Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
}
}
@@ -113,8 +104,7 @@
{
private val slack = 0.1
- def paint(gfx: Graphics2D, visualizer: Visualizer,
- edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+ def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
{
val p = visualizer.Coordinates.get_node(edge._1)
val q = visualizer.Coordinates.get_node(edge._2)
@@ -125,7 +115,7 @@
visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
}
- if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
+ if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
else {
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
path.moveTo(p.x, p.y)
@@ -152,17 +142,15 @@
q.x - slack * dx2, q.y - slack * dy2,
q.x, q.y)
- if (dummies)
- ds.foreach(d =>
- Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
+ if (visualizer.show_dummies)
+ ds.foreach(Dummy.paint(gfx, visualizer, _))
gfx.setStroke(default_stroke)
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 (visualizer.arrow_heads)
+ Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
}
}
}
--- a/src/Tools/Graphview/visualizer.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Mon Jan 05 23:33:39 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(val model: Model)
+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,19 @@
/* font rendering information */
- def font_size: Int = 12
- def font(): Font = new Font("Helvetica", Font.PLAIN, font_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)
+ def make_font(): Font =
+ {
+ val family = options.string("graphview_font_family")
+ val size = options.int("graphview_font_size")
+ new Font(family, Font.PLAIN, size)
+ }
/* rendering parameters */
+ // owned by GUI thread
var arrow_heads = false
+ var show_dummies = false
object Colors
{
@@ -105,12 +76,17 @@
}
}
+ def paint_all_visible(gfx: Graphics2D)
+ {
+ gfx.setRenderingHints(Metrics.rendering_hints)
+ for (edge <- visible_graph.edges_iterator)
+ Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+ for (node <- visible_graph.keys_iterator)
+ Shapes.Node.paint(gfx, visualizer, node)
+ }
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)
@@ -133,54 +109,36 @@
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)
- 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
+ ((for (node <- visible_graph.keys_iterator) yield Shapes.Node.shape(visualizer, node)) ++
+ (for (d <- layout.dummies_iterator) yield Shapes.Dummy.shape(visualizer, d))).
+ foreach(rect => {
+ x0 = x0 min rect.getMinX
+ y0 = y0 min rect.getMinY
+ x1 = x1 max rect.getMaxX
+ y1 = y1 max rect.getMaxY
+ })
+ 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)
}
}
- object Drawer
- {
- def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
- if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
-
- def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
- Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
-
- def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
- {
- gfx.setFont(font())
- gfx.setRenderingHints(rendering_hints)
- val visible_graph = model.make_visible_graph()
- 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)
- }
-
object Selection
{
// owned by GUI thread
--- a/src/Tools/jEdit/etc/options Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/etc/options Mon Jan 05 23:33:39 2015 +0100
@@ -10,13 +10,13 @@
-- "load all required files automatically to resolve theory imports"
public option jedit_reset_font_size : int = 18
- -- "reset font size for main text area"
+ -- "reset main text font size"
public option jedit_font_scale : real = 1.0
- -- "scale factor of add-on panels wrt. main text area"
+ -- "scale factor of add-on panels wrt. main text font"
public option jedit_popup_font_scale : real = 0.85
- -- "scale factor of popups wrt. main text area"
+ -- "scale factor of popups wrt. main text font"
public option jedit_popup_bounds : real = 0.5
-- "relative bounds of popup window wrt. logical screen size"
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Jan 05 23:33:39 2015 +0100
@@ -10,7 +10,7 @@
import isabelle._
import javax.swing.JComponent
-import java.awt.Point
+import java.awt.{Point, Font}
import java.awt.event.{WindowFocusListener, WindowEvent}
import org.gjt.sp.jedit.View
@@ -62,7 +62,7 @@
graph_result match {
case Exn.Res(graph) =>
val model = new isabelle.graphview.Model(graph)
- val visualizer = new isabelle.graphview.Visualizer(model) {
+ val visualizer = new isabelle.graphview.Visualizer(PIDE.options.value, model) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
Pretty_Tooltip.invoke(() =>
@@ -77,21 +77,41 @@
override def background_color = view.getTextArea.getPainter.getBackground
override def selection_color = view.getTextArea.getPainter.getSelectionColor
override def error_color = PIDE.options.color_value("error_color")
- override def font_size = view.getTextArea.getPainter.getFont.getSize
- override def font = view.getTextArea.getPainter.getFont
+
+ override def make_font(): Font =
+ GUI.imitate_font(Font_Info.main().font,
+ PIDE.options.string("graphview_font_family"),
+ PIDE.options.real("graphview_font_scale"))
}
new isabelle.graphview.Main_Panel(model, visualizer)
case Exn.Exn(exn) => new TextArea(Exn.message(exn))
}
set_content(graphview)
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Global_Options](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later {
+ graphview match {
+ case main_panel: isabelle.graphview.Main_Panel =>
+ main_panel.graph_panel.apply_layout()
+ case _ =>
+ }
+ }
+ }
+
override def init()
{
GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+ PIDE.session.global_options += main
}
override def exit()
{
GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+ PIDE.session.global_options -= main
}
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Jan 05 23:33:39 2015 +0100
@@ -32,7 +32,7 @@
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
{
- private val css = GUI.imitate_font_css(Font_Info.main_family(), (new JLabel).getFont)
+ private val css = GUI.imitate_font_css((new JLabel).getFont, Font_Info.main_family())
protected var _name = text
protected var _start = int_to_pos(range.start)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Jan 05 23:33:39 2015 +0100
@@ -201,7 +201,7 @@
})
setColumns(20)
setToolTipText(search_label.tooltip)
- setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+ setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
})
private val search_field_foreground = search_field.foreground
--- a/src/Tools/jEdit/src/query_dockable.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Mon Jan 05 23:33:39 2015 +0100
@@ -48,7 +48,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(tooltip)
- setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+ setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
}
--- a/src/Tools/jEdit/src/token_markup.scala Mon Jan 05 21:48:05 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Jan 05 23:33:39 2015 +0100
@@ -124,7 +124,7 @@
for (idx <- 0 until max_user_fonts)
new_styles(user_font(idx, i.toByte)) = style
for ((family, idx) <- Symbol.font_index)
- new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(family, _))
+ new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
}
new_styles(hidden) =
new SyntaxStyle(hidden_color, null,