# HG changeset patch # User wenzelm # Date 1422468913 -3600 # Node ID 985fc55e9f272f08075c6908e88f818cdced03b8 # Parent 9de8ac92cafa3e02cf6d9b5046fdb0b7f3e858b1 clarified module name; diff -r 9de8ac92cafa -r 985fc55e9f27 src/Pure/build-jars --- a/src/Pure/build-jars Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Pure/build-jars Wed Jan 28 19:15:13 2015 +0100 @@ -106,6 +106,7 @@ term_xml.scala "../Tools/Graphview/graph_file.scala" "../Tools/Graphview/graph_panel.scala" + "../Tools/Graphview/graphview.scala" "../Tools/Graphview/layout.scala" "../Tools/Graphview/main_panel.scala" "../Tools/Graphview/metrics.scala" @@ -116,7 +117,6 @@ "../Tools/Graphview/popups.scala" "../Tools/Graphview/shapes.scala" "../Tools/Graphview/tree_panel.scala" - "../Tools/Graphview/visualizer.scala" ) diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/graph_file.scala --- a/src/Tools/Graphview/graph_file.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/graph_file.scala Wed Jan 28 19:15:13 2015 +0100 @@ -15,9 +15,9 @@ object Graph_File { - def write(file: JFile, visualizer: Visualizer) + def write(file: JFile, graphview: Graphview) { - val box = visualizer.bounding_box() + val box = graphview.bounding_box() val w = box.width.ceil.toInt val h = box.height.ceil.toInt @@ -26,7 +26,7 @@ gfx.setColor(Color.WHITE) gfx.fillRect(0, 0, w, h) gfx.translate(- box.x, - box.y) - visualizer.paint_all_visible(gfx) + graphview.paint_all_visible(gfx) } val name = file.getName @@ -40,9 +40,9 @@ val model = new Model(graph.transitive_reduction_acyclic) val the_options = options - val visualizer = new Visualizer(model) { def options = the_options } - visualizer.update_layout() + val graphview = new Graphview(model) { def options = the_options } + graphview.update_layout() - write(file, visualizer) + write(file, graphview) } } diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Wed Jan 28 19:15:13 2015 +0100 @@ -20,7 +20,7 @@ import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent} -class Graph_Panel(val visualizer: Visualizer) extends BorderPanel +class Graph_Panel(val graphview: Graphview) extends BorderPanel { graph_panel => @@ -36,17 +36,17 @@ { super.paintComponent(gfx) - gfx.setColor(visualizer.background_color) + gfx.setColor(graphview.background_color) gfx.fillRect(0, 0, peer.getWidth, peer.getHeight) gfx.transform(Transform()) - visualizer.paint_all_visible(gfx) + graphview.paint_all_visible(gfx) } } def set_preferred_size() { - val box = visualizer.bounding_box() + val box = graphview.bounding_box() val s = Transform.scale_discrete painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt) painter.revalidate() @@ -62,8 +62,8 @@ def scroll_to_node(node: Graph_Display.Node) { - val gap = visualizer.metrics.gap - val info = visualizer.layout.get_node(node) + val gap = graphview.metrics.gap + val info = graphview.layout.get_node(node) val t = Transform() val p = @@ -84,12 +84,12 @@ override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { override def getToolTipText(event: java.awt.event.MouseEvent): String = - visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { + graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match { case Some(node) => - visualizer.model.full_graph.get_node(node) match { + graphview.model.full_graph.get_node(node) match { case Nil => null case content => - visualizer.make_tooltip(graph_pane.peer, event.getX, event.getY, content) + graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content) } case None => null } @@ -144,13 +144,13 @@ def scale_discrete: Double = { - val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt + val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt (scale * font_height).floor / font_height } def apply() = { - val box = visualizer.bounding_box() + val box = graphview.bounding_box() val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) t.translate(- box.x, - box.y) t @@ -158,10 +158,10 @@ def fit_to_window() { - if (visualizer.visible_graph.is_empty) + if (graphview.visible_graph.is_empty) rescale(1.0) else { - val box = visualizer.bounding_box() + val box = graphview.bounding_box() rescale((size.width / box.width) min (size.height / box.height)) } } @@ -179,8 +179,8 @@ /* interaction */ - visualizer.model.Colors.events += { case _ => painter.repaint() } - visualizer.model.Mutators.events += { case _ => painter.repaint() } + graphview.model.Colors.events += { case _ => painter.repaint() } + graphview.model.Mutators.events += { case _ => painter.repaint() } private object Mouse_Interaction { @@ -191,15 +191,15 @@ { val c = Transform.pane_to_graph_coordinates(at) val l = - visualizer.find_node(c) match { + graphview.find_node(c) match { case Some(node) => - if (visualizer.Selection.contains(node)) visualizer.Selection.get() + if (graphview.Selection.contains(node)) graphview.Selection.get() else List(node) case None => Nil } val d = l match { - case Nil => visualizer.find_dummy(c).toList + case Nil => graphview.find_dummy(c).toList case _ => Nil } draginfo = (at, l, d) @@ -220,10 +220,10 @@ painter.peer.scrollRectToVisible(r) case (Nil, ds) => - ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s)) + ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s)) case (ls, _) => - ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s)) + ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s)) } draginfo = (to, p, d) @@ -237,23 +237,23 @@ if (right_click) { // FIXME if (false) { - val menu = Popups(graph_panel, visualizer.find_node(c), visualizer.Selection.get()) + val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get()) menu.show(graph_pane.peer, at.x, at.y) } } else { - (visualizer.find_node(c), m) match { - case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node) + (graphview.find_node(c), m) match { + case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node) case (None, Key.Modifier.Control) => - case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node) + case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node) case (None, Key.Modifier.Shift) => case (Some(node), _) => - visualizer.Selection.clear() - visualizer.Selection.add(node) + graphview.Selection.clear() + graphview.Selection.add(node) case (None, _) => - visualizer.Selection.clear() + graphview.Selection.clear() } } } @@ -265,9 +265,9 @@ /** controls **/ private val mutator_dialog = - new Mutator_Dialog(visualizer, visualizer.model.Mutators, "Filters", "Hide", false) + new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false) private val color_dialog = - new Mutator_Dialog(visualizer, visualizer.model.Colors, "Colorations") + new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations") private val chooser = new FileChooser { fileSelectionMode = FileChooser.SelectionMode.FilesOnly @@ -275,28 +275,28 @@ } private val show_content = new CheckBox() { - selected = visualizer.show_content + selected = graphview.show_content action = Action("Show content") { - visualizer.show_content = selected - visualizer.update_layout() + graphview.show_content = selected + graphview.update_layout() refresh() } tooltip = "Show full node content within graph layout" } private val show_arrow_heads = new CheckBox() { - selected = visualizer.show_arrow_heads + selected = graphview.show_arrow_heads action = Action("Show arrow heads") { - visualizer.show_arrow_heads = selected + graphview.show_arrow_heads = selected painter.repaint() } tooltip = "Draw edges with explicit arrow heads" } private val show_dummies = new CheckBox() { - selected = visualizer.show_dummies + selected = graphview.show_dummies action = Action("Show dummies") { - visualizer.show_dummies = selected + graphview.show_dummies = selected painter.repaint() } tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging" @@ -306,7 +306,7 @@ action = Action("Save image") { chooser.showSaveDialog(this) match { case FileChooser.Result.Approve => - try { Graph_File.write(chooser.selectedFile, visualizer) } + try { Graph_File.write(chooser.selectedFile, graphview) } catch { case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) } @@ -325,7 +325,7 @@ private val update_layout = new Button { action = Action("Update layout") { - visualizer.update_layout() + graphview.update_layout() refresh() } tooltip = "Regenerate graph layout according to built-in algorithm" diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/graphview.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/graphview.scala Wed Jan 28 19:15:13 2015 +0100 @@ -0,0 +1,178 @@ +/* Title: Tools/Graphview/graphview.scala + Author: Markus Kaiser, TU Muenchen + Author: Makarius + +Graphview visualization parameters and GUI state. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.{Font, Color, Shape, Graphics2D} +import java.awt.geom.{Point2D, Rectangle2D} +import javax.swing.JComponent + + +abstract class Graphview(val model: Model) +{ + graphview => + + + def options: Options + + + /* layout state */ + + // owned by GUI thread + private var _layout: Layout = Layout.empty + def layout: Layout = _layout + + def metrics: Metrics = layout.metrics + def visible_graph: Graph_Display.Graph = layout.input_graph + + def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit = + _layout = _layout.translate_vertex(v, dx, dy) + + def find_node(at: Point2D): Option[Graph_Display.Node] = + layout.output_graph.iterator.collectFirst({ + case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node + }) + + def find_dummy(at: Point2D): Option[Layout.Dummy] = + layout.output_graph.iterator.collectFirst({ + case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy + }) + + def bounding_box(): Rectangle2D.Double = + { + var x0 = 0.0 + var y0 = 0.0 + var x1 = 0.0 + var y1 = 0.0 + for ((_, (info, _)) <- layout.output_graph.iterator) { + val rect = Shapes.shape(info) + x0 = x0 min rect.getMinX + y0 = y0 min rect.getMinY + x1 = x1 max rect.getMaxX + y1 = y1 max rect.getMaxY + } + x0 = (x0 - metrics.gap).floor + y0 = (y0 - metrics.gap).floor + x1 = (x1 + metrics.gap).ceil + y1 = (y1 + metrics.gap).ceil + new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) + } + + def update_layout() + { + val metrics = Metrics(make_font()) + val visible_graph = model.make_visible_graph() + + def node_text(node: Graph_Display.Node, content: XML.Body): String = + if (show_content) { + val s = + XML.content(Pretty.formatted( + content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric)) + if (s.nonEmpty) s else node.toString + } + else node.toString + + _layout = Layout.make(options, metrics, node_text _, visible_graph) + } + + + /* tooltips */ + + def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null + + + /* main colors */ + + def foreground_color: Color = Color.BLACK + def background_color: Color = Color.WHITE + def selection_color: Color = Color.GREEN + def highlight_color: Color = Color.YELLOW + def error_color: Color = Color.RED + def dummy_color: Color = Color.GRAY + + + /* font rendering information */ + + def make_font(): Font = + { + val family = options.string("graphview_font_family") + val size = options.int("graphview_font_size") + new Font(family, Font.PLAIN, size) + } + + + /* rendering parameters */ + + // owned by GUI thread + var show_content = false + var show_arrow_heads = false + var show_dummies = false + + object Colors + { + private val filter_colors = List( + new Color(0xD9, 0xF2, 0xE2), // blue + new Color(0xFF, 0xE7, 0xD8), // orange + new Color(0xFF, 0xFF, 0xE5), // yellow + new Color(0xDE, 0xCE, 0xFF), // lilac + new Color(0xCC, 0xEB, 0xFF), // turquoise + new Color(0xFF, 0xE5, 0xE5), // red + new Color(0xE5, 0xE5, 0xD9) // green + ) + + private var curr : Int = -1 + def next(): Color = + { + curr = (curr + 1) % filter_colors.length + filter_colors(curr) + } + } + + def paint_all_visible(gfx: Graphics2D) + { + gfx.setRenderingHints(Metrics.rendering_hints) + + for (node <- graphview.current_node) + Shapes.highlight_node(gfx, graphview, node) + + for (edge <- visible_graph.edges_iterator) + Shapes.Cardinal_Spline_Edge.paint(gfx, graphview, edge) + + for (node <- visible_graph.keys_iterator) + Shapes.paint_node(gfx, graphview, node) + } + + var current_node: Option[Graph_Display.Node] = None + + object Selection + { + private val state = Synchronized(List.empty[Graph_Display.Node]) + + def get(): List[Graph_Display.Node] = state.value + def contains(node: Graph_Display.Node): Boolean = get().contains(node) + + def add(node: Graph_Display.Node): Unit = state.change(node :: _) + def clear(): Unit = state.change(_ => Nil) + } + + sealed case class Node_Color(border: Color, background: Color, foreground: Color) + + def node_color(node: Graph_Display.Node): Node_Color = + 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) + + def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color = + if (downwards || show_arrow_heads) foreground_color + else error_color +} \ No newline at end of file diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/main_panel.scala --- a/src/Tools/Graphview/main_panel.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/main_panel.scala Wed Jan 28 19:15:13 2015 +0100 @@ -13,19 +13,19 @@ import scala.swing.{SplitPane, Orientation} -class Main_Panel(visualizer: Visualizer) extends SplitPane(Orientation.Vertical) +class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical) { oneTouchExpandable = true - val graph_panel = new Graph_Panel(visualizer) - val tree_panel = new Tree_Panel(visualizer, graph_panel) + val graph_panel = new Graph_Panel(graphview) + val tree_panel = new Tree_Panel(graphview, graph_panel) leftComponent = tree_panel rightComponent = graph_panel def update_layout() { - visualizer.update_layout() + graphview.update_layout() tree_panel.refresh() graph_panel.refresh() } diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/mutator.scala --- a/src/Tools/Graphview/mutator.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/mutator.scala Wed Jan 28 19:15:13 2015 +0100 @@ -18,8 +18,8 @@ { sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator) - def make(visualizer: Visualizer, m: Mutator): Info = - Info(true, visualizer.Colors.next, m) + def make(graphview: Graphview, m: Mutator): Info = + Info(true, graphview.Colors.next, m) class Graph_Filter( val name: String, diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/mutator_dialog.scala --- a/src/Tools/Graphview/mutator_dialog.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/mutator_dialog.scala Wed Jan 28 19:15:13 2015 +0100 @@ -20,7 +20,7 @@ class Mutator_Dialog( - visualizer: Visualizer, + graphview: Graphview, container: Mutator_Container, caption: String, reverse_caption: String = "Inverse", @@ -117,7 +117,7 @@ private val add_button = new Button { action = Action("Add") { add_panel( - new Mutator_Panel(Mutator.Info(true, visualizer.Colors.next, mutator_box.selection.item))) + new Mutator_Panel(Mutator.Info(true, graphview.Colors.next, mutator_box.selection.item))) } } @@ -246,7 +246,7 @@ def get_mutator: Mutator.Info = { - val model = visualizer.model + val model = graphview.model val m = initials.mutator match { case Mutator.Identity() => @@ -333,7 +333,7 @@ reactions += { case ValueChanged(_) => - foreground = if (check(text)) default_foreground else visualizer.error_color + foreground = if (check(text)) default_foreground else graphview.error_color } def string = text diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/popups.scala Wed Jan 28 19:15:13 2015 +0100 @@ -21,10 +21,10 @@ mouse_node: Option[Graph_Display.Node], selected_nodes: List[Graph_Display.Node]): JPopupMenu = { - val visualizer = graph_panel.visualizer + val graphview = graph_panel.graphview - val add_mutator = visualizer.model.Mutators.add _ - val visible_graph = visualizer.visible_graph + val add_mutator = graphview.model.Mutators.add _ + val visible_graph = graphview.visible_graph def filter_context( nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) = @@ -32,25 +32,25 @@ contents += new MenuItem(new Action("This") { def apply = - add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, false))) + add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false))) }) contents += new MenuItem(new Action("Family") { def apply = - add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, true))) + add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true))) }) contents += new MenuItem(new Action("Parents") { def apply = - add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, true))) + add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true))) }) contents += new MenuItem(new Action("Children") { def apply = - add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false))) + add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false))) }) if (edges) { @@ -80,7 +80,7 @@ new Action(quote(to.toString)) { def apply = add_mutator( - Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) + Mutator.make(graphview, Mutator.Edge_Endpoints((from, to)))) }) } } @@ -99,7 +99,7 @@ new Action(quote(from.toString)) { def apply = add_mutator( - Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to)))) + Mutator.make(graphview, Mutator.Edge_Endpoints((from, to)))) }) } } @@ -114,7 +114,7 @@ popup.add( new MenuItem( - new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) }).peer) + new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer) popup.add(new JPopupMenu.Separator) if (mouse_node.isDefined) { diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/shapes.scala Wed Jan 28 19:15:13 2015 +0100 @@ -23,13 +23,13 @@ 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) + def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) { - val metrics = visualizer.metrics + val metrics = graphview.metrics val extra = metrics.char_width - val info = visualizer.layout.get_node(node) + val info = graphview.layout.get_node(node) - gfx.setColor(visualizer.highlight_color) + gfx.setColor(graphview.highlight_color) gfx.fill(new Rectangle2D.Double( info.x - info.width2 - extra, info.y - info.height2 - extra, @@ -37,11 +37,11 @@ info.height + 2 * extra)) } - def paint_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node) + def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node) { - val metrics = visualizer.metrics - val info = visualizer.layout.get_node(node) - val c = visualizer.node_color(node) + val metrics = graphview.metrics + val info = graphview.layout.get_node(node) + val c = graphview.node_color(node) val s = shape(info) gfx.setColor(c.background) @@ -63,24 +63,24 @@ for (line <- info.lines) { gfx.drawString(line, x, y); y += metrics.height.ceil.toInt } } - def paint_dummy(gfx: Graphics2D, visualizer: Visualizer, info: Layout.Info) + def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info) { gfx.setStroke(default_stroke) - gfx.setColor(visualizer.dummy_color) + gfx.setColor(graphview.dummy_color) gfx.draw(shape(info)) } object Straight_Edge { - def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) + def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) { - val p = visualizer.layout.get_node(edge._1) - val q = visualizer.layout.get_node(edge._2) + val p = graphview.layout.get_node(edge._1) + val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y - visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList + graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) @@ -88,13 +88,13 @@ ds.foreach(d => path.lineTo(d.x, d.y)) path.lineTo(q.x, q.y) - if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _)) + if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) - gfx.setColor(visualizer.edge_color(edge, p.y < q.y)) + gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) - if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) + if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } @@ -102,18 +102,18 @@ { private val slack = 0.1 - def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge) + def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge) { - val p = visualizer.layout.get_node(edge._1) - val q = visualizer.layout.get_node(edge._2) + val p = graphview.layout.get_node(edge._1) + val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y - visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList + graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } - if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge) + if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge) else { val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) @@ -140,13 +140,13 @@ q.x - slack * dx2, q.y - slack * dy2, q.x, q.y) - if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _)) + if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) - gfx.setColor(visualizer.edge_color(edge, p.y < q.y)) + gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) - if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) + if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } } diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/Graphview/tree_panel.scala Wed Jan 28 19:15:13 2015 +0100 @@ -19,22 +19,22 @@ import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action} -class Tree_Panel(val visualizer: Visualizer, graph_panel: Graph_Panel) extends BorderPanel +class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel { /* main actions */ private def selection_action() { if (tree != null) { - visualizer.current_node = None - visualizer.Selection.clear() + graphview.current_node = None + graphview.Selection.clear() val paths = tree.getSelectionPaths if (paths != null) { for (path <- paths if path != null) { path.getLastPathComponent match { case tree_node: DefaultMutableTreeNode => tree_node.getUserObject match { - case node: Graph_Display.Node => visualizer.Selection.add(node) + case node: Graph_Display.Node => graphview.Selection.add(node) case _ => } case _ => @@ -58,7 +58,7 @@ case _ => None } action_node.foreach(graph_panel.scroll_to_node(_)) - visualizer.current_node = action_node + graphview.current_node = action_node graph_panel.repaint() } } @@ -111,7 +111,7 @@ private val selection_field_foreground = selection_field.foreground private val selection_delay = - GUI_Thread.delay_last(visualizer.options.seconds("editor_input_delay")) { + GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) { val (pattern, ok) = selection_field.text match { case null | "" => (None, true) @@ -127,7 +127,7 @@ tree.repaint() } selection_field.foreground = - if (ok) selection_field_foreground else visualizer.error_color + if (ok) selection_field_foreground else graphview.error_color } selection_field.peer.getDocument.addDocumentListener(new DocumentListener { @@ -149,7 +149,7 @@ def refresh() { - val new_nodes = visualizer.visible_graph.topological_order + val new_nodes = graphview.visible_graph.topological_order if (new_nodes != nodes) { nodes = new_nodes diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/Graphview/visualizer.scala --- a/src/Tools/Graphview/visualizer.scala Wed Jan 28 08:29:08 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,178 +0,0 @@ -/* Title: Tools/Graphview/visualizer.scala - Author: Markus Kaiser, TU Muenchen - Author: Makarius - -Graph visualization parameters and GUI state. -*/ - -package isabelle.graphview - - -import isabelle._ - -import java.awt.{Font, Color, Shape, Graphics2D} -import java.awt.geom.{Point2D, Rectangle2D} -import javax.swing.JComponent - - -abstract class Visualizer(val model: Model) -{ - visualizer => - - - def options: Options - - - /* layout state */ - - // owned by GUI thread - private var _layout: Layout = Layout.empty - def layout: Layout = _layout - - def metrics: Metrics = layout.metrics - def visible_graph: Graph_Display.Graph = layout.input_graph - - def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit = - _layout = _layout.translate_vertex(v, dx, dy) - - def find_node(at: Point2D): Option[Graph_Display.Node] = - layout.output_graph.iterator.collectFirst({ - case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node - }) - - def find_dummy(at: Point2D): Option[Layout.Dummy] = - layout.output_graph.iterator.collectFirst({ - case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy - }) - - def bounding_box(): Rectangle2D.Double = - { - var x0 = 0.0 - var y0 = 0.0 - var x1 = 0.0 - var y1 = 0.0 - for ((_, (info, _)) <- layout.output_graph.iterator) { - val rect = Shapes.shape(info) - x0 = x0 min rect.getMinX - y0 = y0 min rect.getMinY - x1 = x1 max rect.getMaxX - y1 = y1 max rect.getMaxY - } - x0 = (x0 - metrics.gap).floor - y0 = (y0 - metrics.gap).floor - x1 = (x1 + metrics.gap).ceil - y1 = (y1 + metrics.gap).ceil - new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0) - } - - def update_layout() - { - val metrics = Metrics(make_font()) - val visible_graph = model.make_visible_graph() - - def node_text(node: Graph_Display.Node, content: XML.Body): String = - if (show_content) { - val s = - XML.content(Pretty.formatted( - content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric)) - if (s.nonEmpty) s else node.toString - } - else node.toString - - _layout = Layout.make(options, metrics, node_text _, visible_graph) - } - - - /* tooltips */ - - def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null - - - /* main colors */ - - def foreground_color: Color = Color.BLACK - def background_color: Color = Color.WHITE - def selection_color: Color = Color.GREEN - def highlight_color: Color = Color.YELLOW - def error_color: Color = Color.RED - def dummy_color: Color = Color.GRAY - - - /* font rendering information */ - - def make_font(): Font = - { - val family = options.string("graphview_font_family") - val size = options.int("graphview_font_size") - new Font(family, Font.PLAIN, size) - } - - - /* rendering parameters */ - - // owned by GUI thread - var show_content = false - var show_arrow_heads = false - var show_dummies = false - - object Colors - { - private val filter_colors = List( - new Color(0xD9, 0xF2, 0xE2), // blue - new Color(0xFF, 0xE7, 0xD8), // orange - new Color(0xFF, 0xFF, 0xE5), // yellow - new Color(0xDE, 0xCE, 0xFF), // lilac - new Color(0xCC, 0xEB, 0xFF), // turquoise - new Color(0xFF, 0xE5, 0xE5), // red - new Color(0xE5, 0xE5, 0xD9) // green - ) - - private var curr : Int = -1 - def next(): Color = - { - curr = (curr + 1) % filter_colors.length - filter_colors(curr) - } - } - - 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) - } - - var current_node: Option[Graph_Display.Node] = None - - object Selection - { - private val state = Synchronized(List.empty[Graph_Display.Node]) - - def get(): List[Graph_Display.Node] = state.value - def contains(node: Graph_Display.Node): Boolean = get().contains(node) - - def add(node: Graph_Display.Node): Unit = state.change(node :: _) - def clear(): Unit = state.change(_ => Nil) - } - - sealed case class Node_Color(border: Color, background: Color, foreground: Color) - - def node_color(node: Graph_Display.Node): Node_Color = - 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) - - def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color = - if (downwards || show_arrow_heads) foreground_color - else error_color -} \ No newline at end of file diff -r 9de8ac92cafa -r 985fc55e9f27 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 08:29:08 2015 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 19:15:13 2015 +0100 @@ -62,7 +62,7 @@ graph_result match { case Exn.Res(graph) => val model = new isabelle.graphview.Model(graph) - val visualizer = new isabelle.graphview.Visualizer(model) { + val graphview = new isabelle.graphview.Graphview(model) { def options: Options = PIDE.options.value override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = @@ -86,7 +86,7 @@ override def highlight_color = view.getTextArea.getPainter.getLineHighlightColor override def error_color = PIDE.options.color_value("error_color") } - new isabelle.graphview.Main_Panel(visualizer) + new isabelle.graphview.Main_Panel(graphview) case Exn.Exn(exn) => new TextArea(Exn.message(exn)) } set_content(graphview)