# HG changeset patch
# User wenzelm
# Date 1355224640 -3600
# Node ID 6ee044e2d1a7b815a678f2ee01afb3cf72c60a00
# Parent  ca4088bf836561b7707feaea6750e88b3587ba4f
initial layout coordinates more like old browser;
tuned geometry defaults;

diff -r ca4088bf8365 -r 6ee044e2d1a7 src/Tools/Graphview/src/graph_panel.scala
--- 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()
     }
 
diff -r ca4088bf8365 -r 6ee044e2d1a7 src/Tools/Graphview/src/layout_pendulum.scala
--- 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
               }
             }
 
diff -r ca4088bf8365 -r 6ee044e2d1a7 src/Tools/Graphview/src/parameters.scala
--- 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
diff -r ca4088bf8365 -r 6ee044e2d1a7 src/Tools/Graphview/src/shapes.scala
--- 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
diff -r ca4088bf8365 -r 6ee044e2d1a7 src/Tools/Graphview/src/visualizer.scala
--- 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(