# HG changeset patch
# User wenzelm
# Date 1420291747 -3600
# Node ID fda4091cc6b0f82e5d7e2d1e8f01834d2aa16839
# Parent  541b95e94dc70bd6e8924d85994186c838f11c1a
prefer integer coordinates;
tuned painting;

diff -r 541b95e94dc7 -r fda4091cc6b0 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 13:11:10 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 14:29:07 2015 +0100
@@ -23,7 +23,7 @@
   object Growing_Node extends Node
   {
     private val stroke =
-      new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
     def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String])
       : Rectangle2D.Double =
@@ -32,27 +32,29 @@
       val bounds = m.string_bounds(visualizer.Caption(peer.get))
       val w = bounds.getWidth + m.pad
       val h = bounds.getHeight + m.pad
-      new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
+      new Rectangle2D.Double((x - (w / 2)).floor, (y - (h / 2)).floor, w.ceil, h.ceil)
     }
 
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
     {
+      val m = Visualizer.Metrics(g)
+      val s = shape(m, visualizer, peer)
+      val c = visualizer.node_color(peer)
+
       val caption = visualizer.Caption(peer.get)
-      val m = Visualizer.Metrics(g)
       val bounds = m.string_bounds(caption)
 
-      val s = shape(m, visualizer, peer)
-
-      val c = visualizer.node_color(peer)
-      g.setStroke(stroke)
-      g.setColor(c.border)
-      g.draw(s)
       g.setColor(c.background)
       g.fill(s)
+
+      g.setColor(c.border)
+      g.setStroke(stroke)
+      g.draw(s)
+
       g.setColor(c.foreground)
       g.drawString(caption,
-        (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
-        (s.getY + m.pad / 2 + m.ascent).toFloat)
+        (s.getCenterX - bounds.getWidth / 2).round.toInt,
+        (s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt)
     }
   }
 
@@ -60,10 +62,13 @@
   {
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-    private val shape = new Rectangle2D.Double(-5, -5, 10, 10)  // FIXME
     private val identity = new AffineTransform()
 
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape = shape
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape =
+    {
+      val w = (m.space_width / 2).ceil
+      new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
+    }
 
     def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
       paint_transformed(g, visualizer, peer, identity)
@@ -71,10 +76,13 @@
     def paint_transformed(g: Graphics2D, visualizer: Visualizer,
       peer: Option[String], at: AffineTransform)
     {
+      val m = Visualizer.Metrics(g)
+      val s = shape(m, visualizer, peer)
+
       val c = visualizer.node_color(peer)
       g.setStroke(stroke)
       g.setColor(c.border)
-      g.draw(at.createTransformedShape(shape))
+      g.draw(at.createTransformedShape(s))
     }
   }
 
diff -r 541b95e94dc7 -r fda4091cc6b0 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 13:11:10 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 14:29:07 2015 +0100
@@ -31,12 +31,12 @@
   class Metrics private(font: Font, font_render_context: FontRenderContext)
   {
     def string_bounds(s: String) = font.getStringBounds(s, font_render_context)
-    private val specimen = string_bounds("mix")
-
-    def char_width: Double = specimen.getWidth / 3
-    def height: Double = specimen.getHeight
+    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 = specimen.getWidth
+    def gap: Double = mix.getWidth
     def pad: Double = char_width
   }
 }
@@ -156,8 +156,8 @@
           val max_width =
             model.current_graph.iterator.map({ case (_, (info, _)) =>
               m.string_bounds(info.name).getWidth }).max
-          val box_distance = max_width + m.pad + m.gap
-          def box_height(n: Int): Double = m.char_width * 1.5 * (5 max n)
+          val box_distance = (max_width + m.pad + m.gap).ceil
+          def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
 
           Layout.make(model.current_graph, box_distance, box_height _)
         }
@@ -177,10 +177,10 @@
         x1 = x1 max shape.getMaxX
         y1 = y1 max shape.getMaxY
       }
-      x0 = x0 - m.gap
-      y0 = y0 - m.gap
-      x1 = x1 + m.gap
-      y1 = y1 + m.gap
+      x0 = (x0 - m.gap).floor
+      y0 = (y0 - m.gap).floor
+      x1 = (x1 + m.gap).ceil
+      y1 = (y1 + m.gap).ceil
       new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
     }
   }