# HG changeset patch # User wenzelm # Date 1420124310 -3600 # Node ID 56b34fc7a015efa1058418cab0d5de6ff6033f22 # Parent 0df87ade7052465e4d2d590b7fd129d7090f1c61 more dynamic visualizer -- re-use Isabelle/jEdit options; clarified iTextField error: like Isabelle/jEdit search field; tuned signature; diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/graph_panel.scala --- 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) } diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/main_panel.scala --- 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) diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/model.scala --- 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) } } diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/mutator.scala --- 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 } diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/mutator_dialog.scala --- 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 diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/popups.scala --- 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) { diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/Graphview/visualizer.scala --- 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 diff -r 0df87ade7052 -r 56b34fc7a015 src/Tools/jEdit/src/graphview_dockable.scala --- 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(() =>