# HG changeset patch
# User wenzelm
# Date 1421697961 -3600
# Node ID 19f396384cbebb6b6e1131a8bcbba14c63d4610e
# Parent  b7cfe12acf2e270d959ecdaa44162f4a9fa3b66f
tuned colors;

diff -r b7cfe12acf2e -r 19f396384cbe src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 19 20:39:01 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 19 21:06:01 2015 +0100
@@ -11,7 +11,8 @@
 import isabelle._
 
 import java.awt.{BasicStroke, Graphics2D, Shape}
-import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
+import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D,
+  RoundRectangle2D, PathIterator}
 
 
 object Shapes
@@ -22,6 +23,20 @@
   def shape(info: Layout.Info): Rectangle2D.Double =
     new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)
 
+  def highlight_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
+  {
+    val metrics = visualizer.metrics
+    val extra = metrics.char_width
+    val info = visualizer.layout.get_node(node)
+
+    gfx.setColor(visualizer.highlight_color)
+    gfx.fill(new Rectangle2D.Double(
+      info.x - info.width2 - extra,
+      info.y - info.height2 - extra,
+      info.width + 2 * extra,
+      info.height + 2 * extra))
+  }
+
   def paint_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
   {
     val metrics = visualizer.metrics
diff -r b7cfe12acf2e -r 19f396384cbe src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 19 20:39:01 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 19 21:06:01 2015 +0100
@@ -93,7 +93,7 @@
   def foreground_color: Color = Color.BLACK
   def background_color: Color = Color.WHITE
   def selection_color: Color = Color.GREEN
-  def current_color: Color = Color.YELLOW
+  def highlight_color: Color = Color.YELLOW
   def error_color: Color = Color.RED
   def dummy_color: Color = Color.GRAY
 
@@ -138,8 +138,13 @@
   def paint_all_visible(gfx: Graphics2D)
   {
     gfx.setRenderingHints(Metrics.rendering_hints)
+
+    for (node <- visualizer.current_node)
+      Shapes.highlight_node(gfx, visualizer, node)
+
     for (edge <- visible_graph.edges_iterator)
       Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+
     for (node <- visible_graph.keys_iterator)
       Shapes.paint_node(gfx, visualizer, node)
   }
@@ -161,10 +166,10 @@
   sealed case class Node_Color(border: Color, background: Color, foreground: Color)
 
   def node_color(node: Graph_Display.Node): Node_Color =
-    if (current_node == Some(node))
-      Node_Color(foreground_color, current_color, foreground_color)
-    else if (Selection.contains(node))
+    if (Selection.contains(node))
       Node_Color(foreground_color, selection_color, foreground_color)
+    else if (current_node == Some(node))
+      Node_Color(foreground_color, highlight_color, foreground_color)
     else
       Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
 
diff -r b7cfe12acf2e -r 19f396384cbe src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 19 20:39:01 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 19 21:06:01 2015 +0100
@@ -83,7 +83,7 @@
 
           override def foreground_color = view.getTextArea.getPainter.getForeground
           override def selection_color = view.getTextArea.getPainter.getSelectionColor
-          override def current_color = view.getTextArea.getPainter.getLineHighlightColor
+          override def highlight_color = view.getTextArea.getPainter.getLineHighlightColor
           override def error_color = PIDE.options.color_value("error_color")
         }
         new isabelle.graphview.Main_Panel(visualizer)