more dynamic visualizer -- re-use Isabelle/jEdit options;
clarified iTextField error: like Isabelle/jEdit search field;
tuned signature;

--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -30,7 +30,7 @@
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
       node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
         case Some(name) =>
-          visualizer.model.complete.get_node(name).content match {
+          visualizer.model.complete_graph.get_node(name).content match {
             case Nil => null
             case content => make_tooltip(panel.peer, event.getX, event.getY, content)
           }

--- a/src/Tools/Graphview/main_panel.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -20,14 +20,11 @@
 import javax.swing.JComponent
 
 
-class Main_Panel(graph: Model.Graph) extends BorderPanel
+class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel
 {
   focusable = true
   requestFocus()
 
-  val model = new Model(graph)
-  val visualizer = new Visualizer(model)
-
   def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
   val graph_panel = new Graph_Panel(visualizer, make_tooltip)
 

--- a/src/Tools/Graphview/model.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/model.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -57,7 +57,7 @@
     isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
 }
 
-class Model(private val graph: Model.Graph)
+class Model(val complete_graph: Model.Graph)
 {
   val Mutators =
     new Mutator_Container(
@@ -74,15 +74,14 @@
         Mutator.Node_Expression(".*", false, false, false),
         Mutator.Node_List(Nil, false, false, false)))
 
-  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
+  def visible_nodes_iterator: Iterator[String] = current_graph.keys_iterator
 
   def visible_edges_iterator: Iterator[(String, String)] =
-    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
+    current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))
 
-  def complete = graph
-  def current: Model.Graph =
-    (graph /: Mutators()) {
-      case (g, m) => if (!m.enabled) g else m.mutator.mutate(graph, g)
+  def current_graph: Model.Graph =
+    (complete_graph /: Mutators()) {
+      case (g, m) => if (!m.enabled) g else m.mutator.mutate(complete_graph, g)
     }
 
   private var _colors = Map.empty[String, Color]
@@ -93,7 +92,7 @@
     _colors =
       (Map.empty[String, Color] /: Colors()) {
         case (colors, m) =>
-          (colors /: m.mutator.mutate(graph, graph).keys_iterator) {
+          (colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
             case (colors, k) => colors + (k -> m.color)
           }
       }

--- a/src/Tools/Graphview/mutator.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -25,7 +25,7 @@
     val description: String,
     pred: Model.Graph => Model.Graph) extends Filter
   {
-    def filter(sub: Model.Graph) : Model.Graph = pred(sub)
+    def filter(graph: Model.Graph) : Model.Graph = pred(graph)
   }
 
   class Graph_Mutator(
@@ -33,7 +33,8 @@
     val description: String,
     pred: (Model.Graph, Model.Graph) => Model.Graph) extends Mutator
   {
-    def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph = pred(complete, sub)
+    def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph =
+      pred(complete_graph, graph)
   }
 
   class Node_Filter(
@@ -141,19 +142,20 @@
       "Add by name",
       "Adds every node whose name matches the regex. " +
       "Adds all relevant edges.",
-      (complete, sub) =>
-        add_node_group(complete, sub,
-          complete.keys.filter(k => (regex.r findFirstIn k).isDefined).toList))
+      (complete_graph, graph) =>
+        add_node_group(complete_graph, graph,
+          complete_graph.keys.filter(k => (regex.r findFirstIn k).isDefined).toList))
 
   case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
     extends Graph_Mutator(
       "Add transitive closure",
       "Adds all family members of all current nodes.",
-      (complete, sub) => {
+      (complete_graph, graph) => {
         val withparents =
-          if (parents) add_node_group(complete, sub, complete.all_preds(sub.keys))
-          else sub
-        if (children) add_node_group(complete, withparents, complete.all_succs(sub.keys))
+          if (parents) add_node_group(complete_graph, graph, complete_graph.all_preds(graph.keys))
+          else graph
+        if (children)
+          add_node_group(complete_graph, withparents, complete_graph.all_succs(graph.keys))
         else withparents
       })
 }
@@ -162,13 +164,13 @@
 {
   val name: String
   val description: String
-  def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
+  def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph
 
   override def toString: String = name
 }
 
 trait Filter extends Mutator
 {
-  def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
-  def filter(sub: Model.Graph) : Model.Graph
+  def mutate(complete_graph: Model.Graph, graph: Model.Graph) = filter(graph)
+  def filter(graph: Model.Graph) : Model.Graph
 }

--- a/src/Tools/Graphview/mutator_dialog.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -288,7 +288,7 @@
           List(
             ("", new iCheckBox("Parents", check_children)),
             ("", new iCheckBox("Children", check_parents)),
-            ("Regex", new iTextField(regex, x => Library.make_regex(x).isEmpty)),
+            ("Regex", new iTextField(regex, x => Library.make_regex(x).isDefined)),
             ("", new iCheckBox(reverse_caption, reverse)))
         case Mutator.Node_List(list, reverse, check_parents, check_children) =>
           List(
@@ -301,7 +301,7 @@
             ("Source", new iTextField(source)),
             ("Destination", new iTextField(dest)))
         case Mutator.Add_Node_Expression(regex) =>
-          List(("Regex", new iTextField(regex, x => Library.make_regex(x).isEmpty)))
+          List(("Regex", new iTextField(regex, x => Library.make_regex(x).isDefined)))
         case Mutator.Add_Transitive_Closure(parents, children) =>
           List(
             ("", new iCheckBox("Parents", parents)),
@@ -316,18 +316,16 @@
     def get_bool: Boolean
   }
 
-  private class iTextField(t: String, colorator: String => Boolean)
-  extends TextField(t) with Mutator_Input_Value
+  private class iTextField(t: String, check: String => Boolean = (_: String) => true)
+    extends TextField(t) with Mutator_Input_Value
   {
-    def this(t: String) = this(t, x => false)
-
     preferredSize = new Dimension(125, 18)
 
+    private val default_foreground = foreground
     reactions +=
     {
       case ValueChanged(_) =>
-        if (colorator(text)) background = Color.RED
-        else background = Color.WHITE
+        foreground = if (check(text)) default_foreground else visualizer.error_color
     }
 
     def get_string = text

--- a/src/Tools/Graphview/popups.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -20,7 +20,7 @@
     val visualizer = panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
-    val curr = visualizer.model.current
+    val curr = visualizer.model.current_graph
 
     def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) =
       new Menu(caption) {

--- a/src/Tools/Graphview/visualizer.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -19,6 +19,15 @@
   visualizer =>
 
 
+  /* main colors */
+
+  def foreground_color: Color = Color.BLACK
+  def foreground1_color: Color = Color.GRAY
+  def background_color: Color = Color.WHITE
+  def selection_color: Color = Color.GREEN
+  def error_color: Color = Color.RED
+
+
   /* font rendering information */
 
   val font_family: String = "IsabelleText"
@@ -119,15 +128,15 @@
     def update_layout()
     {
       layout =
-        if (model.current.is_empty) Layout_Pendulum.empty_layout
+        if (model.current_graph.is_empty) Layout_Pendulum.empty_layout
         else {
           val max_width =
-            model.current.iterator.map({ case (_, (info, _)) =>
+            model.current_graph.iterator.map({ case (_, (info, _)) =>
               font_metrics.stringWidth(info.name).toDouble }).max
           val box_distance = max_width + pad_x + gap_x
           def box_height(n: Int): Double =
             ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble
-          Layout_Pendulum(model.current, box_distance, box_height)
+          Layout_Pendulum(model.current_graph, box_distance, box_height)
         }
     }
 
@@ -196,16 +205,18 @@
 
   def node_color(l: Option[String]): Node_Color =
     l match {
-      case None => Node_Color(Color.GRAY, Color.WHITE, Color.BLACK)
+      case None =>
+        Node_Color(foreground1_color, background_color, foreground_color)
+      case Some(c) if Selection(c) =>
+        Node_Color(foreground_color, selection_color, foreground_color)
       case Some(c) =>
-        if (Selection(c)) Node_Color(Color.BLUE, Color.GREEN, Color.BLACK)
-        else Node_Color(Color.BLACK, model.colors.getOrElse(c, Color.WHITE), Color.BLACK)
+        Node_Color(foreground_color, model.colors.getOrElse(c, background_color), foreground_color)
     }
 
-  def edge_color(e: (String, String)): Color = Color.BLACK
+  def edge_color(e: (String, String)): Color = foreground_color
 
   object Caption
   {
-    def apply(key: String) = model.complete.get_node(key).name
+    def apply(key: String) = model.complete_graph.get_node(key).name
   }
 }
\ No newline at end of file

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 14:53:57 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Thu Jan 01 15:58:30 2015 +0100
@@ -49,18 +49,26 @@
 class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
 {
   private val snapshot = Graphview_Dockable.implicit_snapshot
-  private val graph = Graphview_Dockable.implicit_graph
+  private val graph_result = Graphview_Dockable.implicit_graph
 
   private val window_focus_listener =
     new WindowFocusListener {
-      def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) }
+      def windowGainedFocus(e: WindowEvent) {
+        Graphview_Dockable.set_implicit(snapshot, graph_result) }
       def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
     }
 
   val graphview =
-    graph match {
-      case Exn.Res(proper_graph) =>
-        new isabelle.graphview.Main_Panel(proper_graph) {
+    graph_result match {
+      case Exn.Res(graph) =>
+        val model = new isabelle.graphview.Model(graph)
+        val visualizer = new isabelle.graphview.Visualizer(model) {
+          override def foreground_color = view.getTextArea.getPainter.getForeground
+          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")
+        }
+        new isabelle.graphview.Main_Panel(model, visualizer) {
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             Pretty_Tooltip.invoke(() =>