--- a/src/Tools/Graphview/src/graph_panel.scala Tue Dec 11 10:35:42 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala Tue Dec 11 12:17:20 2012 +0100
@@ -112,13 +112,13 @@
private object Transform
{
- val padding = (4000, 2000)
+ val padding = (100, 40)
- private var _scale = 1.0
+ private var _scale: Double = 1.0
def scale = _scale
def scale_= (s: Double) =
{
- _scale = (s min 10) max 0.01
+ _scale = (s min 10) max 0.1
paint_panel.set_preferred_size()
}
--- a/src/Tools/Graphview/src/layout_pendulum.scala Tue Dec 11 10:35:42 2012 +0100
+++ b/src/Tools/Graphview/src/layout_pendulum.scala Tue Dec 11 12:17:20 2012 +0100
@@ -22,12 +22,10 @@
case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]])
val empty_layout = Layout(Map.empty, Map.empty)
- val x_distance = 350
- val y_distance = 350
val pendulum_iterations = 10
val minimize_crossings_iterations = 40
- def apply(graph: Model.Graph): Layout =
+ def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout =
{
if (graph.is_empty) empty_layout
else {
@@ -48,7 +46,17 @@
val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
- val coords = pendulum(dummy_graph, levels, initial_coordinates(levels))
+ val initial_coordinates: Coordinates =
+ (((Map.empty[Key, Point], 0.0) /: levels) {
+ case ((coords1, y), level) =>
+ ((((coords1, 0.0) /: level) {
+ case ((coords2, x), key) =>
+ val s = if (graph.defined(key)) graph.get_node(key).name else "X"
+ (coords2 + (key -> (x, y)), x + box_distance)
+ })._1, y + box_height(level.length))
+ })._1
+
+ val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)
val dummy_coords =
(Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
@@ -153,16 +161,8 @@
}._1
}
- def initial_coordinates(levels: Levels): Coordinates =
- (Map.empty[Key, Point] /: levels.zipWithIndex){
- case (coords, (level, yi)) =>
- (coords /: level.zipWithIndex) {
- case (coords, (node, xi)) =>
- coords + (node -> (xi * x_distance, yi * y_distance))
- }
- }
-
- def pendulum(graph: Model.Graph, levels: Levels, coords: Map[Key, Point]): Coordinates =
+ def pendulum(graph: Model.Graph, box_distance: Double,
+ levels: Levels, coords: Map[Key, Point]): Coordinates =
{
type Regions = List[List[Region]]
@@ -196,7 +196,7 @@
val d2 = r2.deflection(coords, top_down)
if (// Do regions touch?
- r1.distance(coords, r2) <= x_distance &&
+ r1.distance(coords, r2) <= box_distance &&
// Do they influence each other?
(d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0))
{
@@ -222,11 +222,11 @@
else if (i == level.length - 1 && d >= 0) d
else if (d < 0) {
val prev = level(i-1)
- (-(r.distance(coords, prev) - x_distance)) max d
+ (-(r.distance(coords, prev) - box_distance)) max d
}
else {
val next = level(i+1)
- (r.distance(coords, next) - x_distance) min d
+ (r.distance(coords, next) - box_distance) min d
}
}
--- a/src/Tools/Graphview/src/parameters.scala Tue Dec 11 10:35:42 2012 +0100
+++ b/src/Tools/Graphview/src/parameters.scala Tue Dec 11 12:17:20 2012 +0100
@@ -14,7 +14,11 @@
class Parameters
{
val font_family: String = "IsabelleText"
- val font_size: Int = 16
+ val font_size: Int = 14
+ val gap_x = 20
+ val pad_x = 8
+ val pad_y = 5
+
val tooltip_font_size: Int = 10
var arrow_heads = false
--- a/src/Tools/Graphview/src/shapes.scala Tue Dec 11 10:35:42 2012 +0100
+++ b/src/Tools/Graphview/src/shapes.scala Tue Dec 11 12:17:20 2012 +0100
@@ -26,16 +26,11 @@
def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
{
- val caption = visualizer.Caption(peer.get)
- val bounds = g.getFontMetrics.getStringBounds(caption, g)
val (x, y) = visualizer.Coordinates(peer.get)
-
- new Rectangle2D.Double(
- x -(bounds.getWidth / 2 + 25),
- y -(bounds.getHeight / 2 + 5),
- bounds.getWidth + 50,
- bounds.getHeight + 10
- )
+ val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
+ val w = bounds.getWidth + visualizer.parameters.pad_x
+ val h = bounds.getHeight + visualizer.parameters.pad_y
+ new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
}
def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
@@ -61,7 +56,7 @@
{
private val stroke =
new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
- private val shape = new Rectangle2D.Double(-8, -8, 16, 16)
+ private val shape = new Rectangle2D.Double(-5, -5, 10, 10)
private val identity = new AffineTransform()
def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape
--- a/src/Tools/Graphview/src/visualizer.scala Tue Dec 11 10:35:42 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Tue Dec 11 12:17:20 2012 +0100
@@ -10,8 +10,7 @@
import isabelle._
-import java.awt.{Font, Color => JColor, Shape}
-import java.awt.{RenderingHints, Graphics2D}
+import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D, Toolkit}
import javax.swing.JComponent
@@ -71,7 +70,18 @@
def update_layout()
{
- layout = Layout_Pendulum(model.current) // FIXME avoid computation on Swing thread
+ layout =
+ if (model.current.is_empty) Layout_Pendulum.empty_layout
+ else {
+ val max_width =
+ model.current.entries.map({ case (_, (info, _)) =>
+ font_metrics.stringWidth(info.name).toDouble }).max
+ val box_distance = max_width + parameters.pad_x + parameters.gap_x
+ def box_height(n: Int): Double =
+ ((font_metrics.getAscent + font_metrics.getDescent + parameters.pad_y) * (5 max n))
+ .toDouble
+ Layout_Pendulum(model.current, box_distance, box_height)
+ }
}
def bounds(): (Double, Double, Double, Double) =
@@ -156,7 +166,11 @@
def apply(key: String) = model.complete.get_node(key).name
}
+
+ /* font rendering information */
+
val font = new Font(parameters.font_family, Font.BOLD, parameters.font_size)
+ val font_metrics: FontMetrics = Toolkit.getDefaultToolkit.getFontMetrics(font)
val rendering_hints =
new RenderingHints(