# HG changeset patch # User wenzelm # Date 1419945066 -3600 # Node ID 711c2446dc9dafa607d61bfc49e170cd59574022 # Parent 702e0971d61763487057ac62c320b5176caaea58 clarified source location; diff -r 702e0971d617 -r 711c2446dc9d src/Pure/build-jars --- a/src/Pure/build-jars Tue Dec 30 11:50:34 2014 +0100 +++ b/src/Pure/build-jars Tue Dec 30 14:11:06 2014 +0100 @@ -102,16 +102,16 @@ library.scala term.scala term_xml.scala - "../Tools/Graphview/src/graph_panel.scala" - "../Tools/Graphview/src/layout_pendulum.scala" - "../Tools/Graphview/src/main_panel.scala" - "../Tools/Graphview/src/model.scala" - "../Tools/Graphview/src/mutator_dialog.scala" - "../Tools/Graphview/src/mutator_event.scala" - "../Tools/Graphview/src/mutator.scala" - "../Tools/Graphview/src/popups.scala" - "../Tools/Graphview/src/shapes.scala" - "../Tools/Graphview/src/visualizer.scala" + "../Tools/Graphview/graph_panel.scala" + "../Tools/Graphview/layout_pendulum.scala" + "../Tools/Graphview/main_panel.scala" + "../Tools/Graphview/model.scala" + "../Tools/Graphview/mutator_dialog.scala" + "../Tools/Graphview/mutator_event.scala" + "../Tools/Graphview/mutator.scala" + "../Tools/Graphview/popups.scala" + "../Tools/Graphview/shapes.scala" + "../Tools/Graphview/visualizer.scala" ) diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/graph_panel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/graph_panel.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,298 @@ +/* Title: Tools/Graphview/graph_panel.scala + Author: Markus Kaiser, TU Muenchen + +Graphview Java2D drawing panel. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.{Dimension, Graphics2D, Point, Rectangle} +import java.awt.geom.{AffineTransform, Point2D} +import java.awt.image.BufferedImage +import javax.swing.{JScrollPane, JComponent} + +import scala.swing.{Panel, ScrollPane} +import scala.swing.event._ + + +class Graph_Panel( + val visualizer: Visualizer, + make_tooltip: (JComponent, Int, Int, XML.Body) => String) + extends ScrollPane +{ + panel => + + tooltip = "" + + override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { + 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 { + case Nil => null + case content => make_tooltip(panel.peer, event.getX, event.getY, content) + } + case None => null + } + } + + peer.setWheelScrollingEnabled(false) + focusable = true + requestFocus() + + horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always + verticalScrollBarPolicy = ScrollPane.BarPolicy.Always + + def node(at: Point2D): Option[String] = + visualizer.model.visible_nodes_iterator + .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at)) + + def refresh() + { + if (paint_panel != null) { + paint_panel.set_preferred_size() + paint_panel.repaint() + } + } + + def fit_to_window() = { + Transform.fit_to_window() + refresh() + } + + val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } + + def rescale(s: Double) + { + Transform.scale = s + if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt) + refresh() + } + + def apply_layout() = visualizer.Coordinates.update_layout() + + private class Paint_Panel extends Panel { + def set_preferred_size() { + val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() + val s = Transform.scale_discrete + val (px, py) = Transform.padding + + preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt, + (math.abs(maxY - minY + py) * s).toInt) + + revalidate() + } + + override def paint(g: Graphics2D) { + super.paintComponent(g) + g.transform(Transform()) + + visualizer.Drawer.paint_all_visible(g, true) + } + } + private val paint_panel = new Paint_Panel + contents = paint_panel + + listenTo(keys) + listenTo(mouse.moves) + listenTo(mouse.clicks) + listenTo(mouse.wheel) + reactions += Interaction.Mouse.react + reactions += Interaction.Keyboard.react + reactions += { + case KeyTyped(_, _, _, _) => {repaint(); requestFocus()} + case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()} + case MouseDragged(_, _, _) => {repaint(); requestFocus()} + case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()} + case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()} + case MouseMoved(_, _, _) => repaint() + } + + visualizer.model.Colors.events += { case _ => repaint() } + visualizer.model.Mutators.events += { case _ => repaint() } + + apply_layout() + rescale(1.0) + + private object Transform + { + val padding = (100, 40) + + private var _scale: Double = 1.0 + def scale: Double = _scale + def scale_=(s: Double) + { + _scale = (s min 10) max 0.1 + } + def scale_discrete: Double = + (_scale * visualizer.font_size).round.toDouble / visualizer.font_size + + def apply() = { + val (minX, minY, _, _) = visualizer.Coordinates.bounds() + + val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) + at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2) + at + } + + def fit_to_window() { + if (visualizer.model.visible_nodes_iterator.isEmpty) + rescale(1.0) + else { + val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() + + val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2) + val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy) + rescale(sx min sy) + } + } + + def pane_to_graph_coordinates(at: Point2D): Point2D = { + val s = Transform.scale_discrete + val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null) + + p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s) + p + } + } + + object Interaction { + object Keyboard { + import scala.swing.event.Key._ + + val react: PartialFunction[Event, Unit] = { + case KeyTyped(_, c, m, _) => typed(c, m) + } + + def typed(c: Char, m: Modifiers) = + (c, m) match { + case ('+', _) => rescale(Transform.scale * 5.0/4) + case ('-', _) => rescale(Transform.scale * 4.0/5) + case ('0', _) => Transform.fit_to_window() + case ('1', _) => visualizer.Coordinates.update_layout() + case ('2', _) => Transform.fit_to_window() + case _ => + } + } + + object Mouse { + import scala.swing.event.Key.Modifier._ + type Modifiers = Int + type Dummy = ((String, String), Int) + + private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null + + val react: PartialFunction[Event, Unit] = { + case MousePressed(_, p, _, _, _) => pressed(p) + case MouseDragged(_, to, _) => { + drag(draginfo, to) + val (_, p, d) = draginfo + draginfo = (to, p, d) + } + case MouseWheelMoved(_, p, _, r) => wheel(r, p) + case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e) + } + + def dummy(at: Point2D): Option[Dummy] = + visualizer.model.visible_edges_iterator.map({ + i => visualizer.Coordinates(i).zipWithIndex.map((i, _)) + }).flatten.find({ + case (_, ((x, y), _)) => + visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y) + }) match { + case None => None + case Some((name, (_, index))) => Some((name, index)) + } + + def pressed(at: Point) { + val c = Transform.pane_to_graph_coordinates(at) + val l = node(c) match { + case Some(l) => + if (visualizer.Selection(l)) visualizer.Selection() else List(l) + case None => Nil + } + val d = l match { + case Nil => dummy(c) match { + case Some(d) => List(d) + case None => Nil + } + + case _ => Nil + } + + draginfo = (at, l, d) + } + + def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) { + import javax.swing.SwingUtilities + + val c = Transform.pane_to_graph_coordinates(at) + val p = node(c) + + def left_click() { + (p, m) match { + case (Some(l), Control) => visualizer.Selection.add(l) + case (None, Control) => + + case (Some(l), Shift) => visualizer.Selection.add(l) + case (None, Shift) => + + case (Some(l), _) => visualizer.Selection.set(List(l)) + case (None, _) => visualizer.Selection.clear + } + } + + def right_click() { + val menu = Popups(panel, p, visualizer.Selection()) + menu.show(panel.peer, at.x, at.y) + } + + if (clicks < 2) { + if (SwingUtilities.isRightMouseButton(e.peer)) right_click() + else left_click() + } + } + + def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) { + val (from, p, d) = draginfo + + val s = Transform.scale_discrete + val (dx, dy) = (to.x - from.x, to.y - from.y) + (p, d) match { + case (Nil, Nil) => { + val r = panel.peer.getViewport.getViewRect + r.translate(-dx, -dy) + + paint_panel.peer.scrollRectToVisible(r) + } + + case (Nil, ds) => + ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s))) + + case (ls, _) => + ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s))) + } + } + + def wheel(rotation: Int, at: Point) { + val at2 = Transform.pane_to_graph_coordinates(at) + // > 0 -> up + rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4)) + + // move mouseposition to center + Transform().transform(at2, at2) + val r = panel.peer.getViewport.getViewRect + val (width, height) = (r.getWidth, r.getHeight) + paint_panel.peer.scrollRectToVisible( + new Rectangle((at2.getX() - width / 2).toInt, + (at2.getY() - height / 2).toInt, + width.toInt, + height.toInt) + ) + } + } + } +} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/layout_pendulum.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/layout_pendulum.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,275 @@ +/* Title: Tools/Graphview/layout_pendulum.scala + Author: Markus Kaiser, TU Muenchen + +Pendulum DAG layout algorithm. +*/ + +package isabelle.graphview + + +import isabelle._ + + +object Layout_Pendulum +{ + type Key = String + type Point = (Double, Double) + type Coordinates = Map[Key, Point] + type Level = List[Key] + type Levels = List[Level] + type Dummies = (Model.Graph, List[Key], Map[Key, Int]) + + case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]]) + val empty_layout = Layout(Map.empty, Map.empty) + + val pendulum_iterations = 10 + val minimize_crossings_iterations = 40 + + def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = + { + if (graph.is_empty) empty_layout + else { + val initial_levels = level_map(graph) + + val (dummy_graph, dummies, dummy_levels) = + ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { + case ((graph, dummies, levels), from) => + ((graph, dummies, levels) /: graph.imm_succs(from)) { + case ((graph, dummies, levels), to) => + if (levels(to) - levels(from) <= 1) (graph, dummies, levels) + else { + val (next, ds, ls) = add_dummies(graph, from, to, levels) + (next, dummies + ((from, to) -> ds), ls) + } + } + } + + val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) + + val initial_coordinates: Coordinates = + (((Map.empty[Key, Point], 0.0) /: levels) { + case ((coords1, y), level) => + ((((coords1, 0.0) /: level) { + case ((coords2, x), key) => + val s = if (graph.defined(key)) graph.get_node(key).name else "X" + (coords2 + (key -> (x, y)), x + box_distance) + })._1, y + box_height(level.length)) + })._1 + + val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) + + val dummy_coords = + (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { + case (map, key) => map + (key -> dummies(key).map(coords(_))) + } + + Layout(coords, dummy_coords) + } + } + + + def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = + { + val ds = + ((levels(from) + 1) until levels(to)) + .map("%s$%s$%d" format (from, to, _)).toList + + val ls = + (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { + case (ls, (l, d)) => ls + (d -> l) + } + + val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) + val graph2 = + (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { + case (g, List(x, y)) => g.add_edge(x, y) + } + (graph2, ds, ls) + } + + def level_map(graph: Model.Graph): Map[Key, Int] = + (Map.empty[Key, Int] /: graph.topological_order) { + (levels, key) => { + val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) } + levels + (key -> lev) + } + } + + def level_list(map: Map[Key, Int]): Levels = + { + val max_lev = (-1 /: map) { case (m, (_, l)) => m max l } + val buckets = new Array[Level](max_lev + 1) + for (l <- 0 to max_lev) { buckets(l) = Nil } + for ((key, l) <- map) { buckets(l) = key :: buckets(l) } + buckets.iterator.map(_.sorted).toList + } + + def count_crossings(graph: Model.Graph, levels: Levels): Int = + { + def in_level(ls: Levels): Int = ls match { + case List(top, bot) => + top.iterator.zipWithIndex.map { + case (outer_parent, outer_parent_index) => + graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) + .map(outer_child => + (0 until outer_parent_index) + .map(inner_parent => + graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) + .filter(inner_child => outer_child < inner_child) + .size + ).sum + ).sum + }.sum + + case _ => 0 + } + + levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum + } + + def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = + { + def resort_level(parent: Level, child: Level, top_down: Boolean): Level = + child.map(k => { + val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) + val weight = + (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) + (k, weight) + }).sortBy(_._2).map(_._1) + + def resort(levels: Levels, top_down: Boolean) = top_down match { + case true => + (List[Level](levels.head) /: levels.tail) { + (tops, bot) => resort_level(tops.head, bot, top_down) :: tops + }.reverse + + case false => + (List[Level](levels.reverse.head) /: levels.reverse.tail) { + (bots, top) => resort_level(bots.head, top, top_down) :: bots + } + } + + ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { + case ((old_levels, old_crossings, top_down), _) => { + val new_levels = resort(old_levels, top_down) + val new_crossings = count_crossings(graph, new_levels) + if (new_crossings < old_crossings) + (new_levels, new_crossings, !top_down) + else + (old_levels, old_crossings, !top_down) + } + }._1 + } + + def pendulum(graph: Model.Graph, box_distance: Double, + levels: Levels, coords: Map[Key, Point]): Coordinates = + { + type Regions = List[List[Region]] + + def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) + : (Regions, Coordinates, Boolean) = + { + val (nextr, nextc, moved) = + ((List.empty[List[Region]], coords, false) /: + (if (top_down) regions else regions.reverse)) { + case ((tops, coords, prev_moved), bot) => { + val nextb = collapse(coords, bot, top_down) + val (nextc, this_moved) = deflect(coords, nextb, top_down) + (nextb :: tops, nextc, prev_moved || this_moved) + } + } + + (nextr.reverse, nextc, moved) + } + + def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = + { + if (level.size <= 1) level + else { + var next = level + var regions_changed = true + while (regions_changed) { + regions_changed = false + for (i <- (next.length to 1)) { + val (r1, r2) = (next(i-1), next(i)) + val d1 = r1.deflection(coords, top_down) + val d2 = r2.deflection(coords, top_down) + + if (// Do regions touch? + r1.distance(coords, r2) <= box_distance && + // Do they influence each other? + (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) + { + regions_changed = true + r1.nodes = r1.nodes ::: r2.nodes + next = next.filter(next.indexOf(_) != i) + } + } + } + next + } + } + + def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) + : (Coordinates, Boolean) = + { + ((coords, false) /: (0 until level.length)) { + case ((coords, moved), i) => { + val r = level(i) + val d = r.deflection(coords, top_down) + val offset = { + if (i == 0 && d <= 0) d + else if (i == level.length - 1 && d >= 0) d + else if (d < 0) { + val prev = level(i-1) + (-(r.distance(coords, prev) - box_distance)) max d + } + else { + val next = level(i+1) + (r.distance(coords, next) - box_distance) min d + } + } + + (r.move(coords, offset), moved || (d != 0)) + } + } + } + + val regions = levels.map(level => level.map(new Region(graph, _))) + + ((regions, coords, true, true) /: (1 to pendulum_iterations)) { + case ((regions, coords, top_down, moved), _) => + if (moved) { + val (nextr, nextc, m) = iteration(regions, coords, top_down) + (nextr, nextc, !top_down, m) + } + else (regions, coords, !top_down, moved) + }._2 + } + + private class Region(val graph: Model.Graph, node: Key) + { + var nodes: List[Key] = List(node) + + def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min + def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max + + def distance(coords: Coordinates, to: Region): Double = + math.abs(left(coords) - to.left(coords)) min + math.abs(right(coords) - to.right(coords)) + + def deflection(coords: Coordinates, use_preds: Boolean) = + nodes.map(k => (coords(k)._1, + if (use_preds) graph.imm_preds(k).toList // FIXME iterator + else graph.imm_succs(k).toList)) + .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) }) + .sum / nodes.length + + def move(coords: Coordinates, by: Double): Coordinates = + (coords /: nodes) { + case (cs, node) => + val (x, y) = cs(node) + cs + (node -> (x + by, y)) + } + } +} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/main_panel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/main_panel.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,125 @@ +/* Title: Tools/Graphview/main_panel.scala + Author: Markus Kaiser, TU Muenchen + +Graph Panel wrapper. +*/ + +package isabelle.graphview + + +import isabelle._ +import isabelle.graphview.Mutators._ + +import scala.collection.JavaConversions._ +import scala.swing.{BorderPanel, Button, BoxPanel, + Orientation, Swing, CheckBox, Action, FileChooser} + +import java.io.{File => JFile} +import java.awt.{Color, Dimension, Graphics2D} +import java.awt.geom.Rectangle2D +import java.awt.image.BufferedImage +import javax.imageio.ImageIO +import javax.swing.border.EmptyBorder +import javax.swing.JComponent + + +class Main_Panel(graph: Model.Graph) 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) + + listenTo(keys) + reactions += graph_panel.reactions + + val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) + + val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations") + + private val chooser = new FileChooser() + chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly + chooser.title = "Save Image (.png or .pdf)" + + val options_panel = new BoxPanel(Orientation.Horizontal) { + border = new EmptyBorder(0, 0, 10, 0) + + contents += Swing.HGlue + contents += new CheckBox(){ + selected = visualizer.arrow_heads + action = Action("Arrow Heads"){ + visualizer.arrow_heads = selected + graph_panel.repaint() + } + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Button{ + action = Action("Save Image"){ + chooser.showSaveDialog(this) match { + case FileChooser.Result.Approve => export(chooser.selectedFile) + case _ => + } + } + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += graph_panel.zoom + + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Button{ + action = Action("Apply Layout"){ + graph_panel.apply_layout() + } + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Button{ + action = Action("Fit to Window"){ + graph_panel.fit_to_window() + } + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Button{ + action = Action("Colorations"){ + color_dialog.open + } + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += new Button{ + action = Action("Filters"){ + mutator_dialog.open + } + } + } + + add(graph_panel, BorderPanel.Position.Center) + add(options_panel, BorderPanel.Position.North) + + private def export(file: JFile) + { + val (x0, y0, x1, y1) = visualizer.Coordinates.bounds + val w = (math.abs(x1 - x0) + 400).toInt + val h = (math.abs(y1 - y0) + 200).toInt + + def paint(gfx: Graphics2D) + { + gfx.setColor(Color.WHITE) + gfx.fill(new Rectangle2D.Double(0, 0, w, h)) + + gfx.translate(- x0 + 200, - y0 + 100) + visualizer.Drawer.paint_all_visible(gfx, false) + } + + try { + val name = file.getName + if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) + else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) + else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") + } + catch { + case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) + } + } +} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/model.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,106 @@ +/* Title: Tools/Graphview/model.scala + Author: Markus Kaiser, TU Muenchen + +Internal graph representation. +*/ + +package isabelle.graphview + + +import isabelle._ +import isabelle.graphview.Mutators._ + +import java.awt.Color + + +class Mutator_Container(val available: List[Mutator]) { + type Mutator_Markup = (Boolean, Color, Mutator) + + val events = new Mutator_Event.Bus + + private var _mutators : List[Mutator_Markup] = Nil + def apply() = _mutators + def apply(mutators: List[Mutator_Markup]){ + _mutators = mutators + + events.event(Mutator_Event.NewList(mutators)) + } + + def add(mutator: Mutator_Markup) = { + _mutators = _mutators ::: List(mutator) + + events.event(Mutator_Event.Add(mutator)) + } +} + + +object Model +{ + /* node info */ + + sealed case class Info(name: String, content: XML.Body) + + val empty_info: Info = Info("", Nil) + + val decode_info: XML.Decode.T[Info] = (body: XML.Body) => + { + import XML.Decode._ + + val (name, content) = pair(string, x => x)(body) + Info(name, content) + } + + + /* graph */ + + type Graph = isabelle.Graph[String, Info] + + val decode_graph: XML.Decode.T[Graph] = + isabelle.Graph.decode(XML.Decode.string, decode_info) +} + +class Model(private val graph: Model.Graph) { + val Mutators = new Mutator_Container( + List( + Node_Expression(".*", false, false, false), + Node_List(Nil, false, false, false), + Edge_Endpoints("", ""), + Add_Node_Expression(""), + Add_Transitive_Closure(true, true) + )) + + val Colors = new Mutator_Container( + List( + Node_Expression(".*", false, false, false), + Node_List(Nil, false, false, false) + )) + + def visible_nodes_iterator: Iterator[String] = current.keys_iterator + + def visible_edges_iterator: Iterator[(String, String)] = + current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _))) + + def complete = graph + def current: Model.Graph = + (graph /: Mutators()) { + case (g, (enabled, _, mutator)) => { + if (!enabled) g + else mutator.mutate(graph, g) + } + } + + private var _colors = Map.empty[String, Color] + def colors = _colors + + private def build_colors() { + _colors = + (Map.empty[String, Color] /: Colors()) ({ + case (colors, (enabled, color, mutator)) => { + (colors /: mutator.mutate(graph, graph).keys_iterator) ({ + case (colors, k) => colors + (k -> color) + }) + } + }) + } + Colors.events += { case _ => build_colors() } +} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/mutator.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/mutator.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,199 @@ +/* Title: Tools/Graphview/mutator.scala + Author: Markus Kaiser, TU Muenchen + +Filters and add-operations on graphs. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.Color +import scala.collection.immutable.SortedSet + + +trait Mutator +{ + val name: String + val description: String + def mutate(complete: Model.Graph, sub: 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 +} + +object Mutators { + type Mutator_Markup = (Boolean, Color, Mutator) + + val Enabled = true + val Disabled = false + + def create(visualizer: Visualizer, m: Mutator): Mutator_Markup = + (Mutators.Enabled, visualizer.Colors.next, m) + + class Graph_Filter(val name: String, val description: String, + pred: Model.Graph => Model.Graph) + extends Filter + { + def filter(sub: Model.Graph) : Model.Graph = pred(sub) + } + + class Graph_Mutator(val name: String, 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) + } + + class Node_Filter(name: String, description: String, + pred: (Model.Graph, String) => Boolean) + extends Graph_Filter ( + + name, + description, + g => g.restrict(pred(g, _)) + ) + + class Edge_Filter(name: String, description: String, + pred: (Model.Graph, String, String) => Boolean) + extends Graph_Filter ( + + name, + description, + g => (g /: g.dest) { + case (graph, ((from, _), tos)) => { + (graph /: tos) { + (gr, to) => if (pred(gr, from, to)) gr + else gr.del_edge(from, to) + } + } + } + ) + + class Node_Family_Filter(name: String, description: String, + reverse: Boolean, parents: Boolean, children: Boolean, + pred: (Model.Graph, String) => Boolean) + extends Node_Filter( + + name, + description, + (g, k) => reverse != ( + pred(g, k) || + (parents && g.all_preds(List(k)).exists(pred(g, _))) || + (children && g.all_succs(List(k)).exists(pred(g, _))) + ) + ) + + case class Identity() + extends Graph_Filter( + + "Identity", + "Does not change the graph.", + g => g + ) + + case class Node_Expression(regex: String, + reverse: Boolean, parents: Boolean, children: Boolean) + extends Node_Family_Filter( + + "Filter by Name", + "Only shows or hides all nodes with any family member's name matching " + + "a regex.", + reverse, + parents, + children, + (g, k) => (regex.r findFirstIn k).isDefined + ) + + case class Node_List(list: List[String], + reverse: Boolean, parents: Boolean, children: Boolean) + extends Node_Family_Filter( + + "Filter by Name List", + "Only shows or hides all nodes with any family member's name matching " + + "any string in a comma separated list.", + reverse, + parents, + children, + (g, k) => list.exists(_ == k) + ) + + case class Edge_Endpoints(source: String, dest: String) + extends Edge_Filter( + + "Hide edge", + "Hides the edge whose endpoints match strings.", + (g, s, d) => !(s == source && d == dest) + ) + + private def add_node_group(from: Model.Graph, to: Model.Graph, + keys: List[String]) = { + + // Add Nodes + val with_nodes = + (to /: keys) { + (graph, key) => graph.default_node(key, from.get_node(key)) + } + + // Add Edges + (with_nodes /: keys) { + (gv, key) => { + def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) = + (g /: keys) { + (graph, end) => { + if (!graph.keys_iterator.contains(end)) graph + else { + if (succs) graph.add_edge(key, end) + else graph.add_edge(end, key) + } + } + } + + + add_edges( + add_edges(gv, from.imm_preds(key), false), + from.imm_succs(key), true + ) + } + } + } + + case class Add_Node_Expression(regex: String) + extends Graph_Mutator( + + "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) + } + ) + + 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) => { + 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)) + else + withparents + } + ) +} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/mutator_dialog.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/mutator_dialog.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,427 @@ +/* Title: Tools/Graphview/mutator_dialog.scala + Author: Markus Kaiser, TU Muenchen + +Mutator selection and configuration dialog. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.Color +import java.awt.FocusTraversalPolicy +import javax.swing.JColorChooser +import javax.swing.border.EmptyBorder +import scala.collection.JavaConversions._ +import scala.swing._ +import isabelle.graphview.Mutators._ +import scala.swing.event.ValueChanged + + +class Mutator_Dialog( + visualizer: Visualizer, + container: Mutator_Container, + caption: String, + reverse_caption: String = "Inverse", + show_color_chooser: Boolean = true) + extends Dialog +{ + type Mutator_Markup = (Boolean, Color, Mutator) + + title = caption + + private var _panels: List[Mutator_Panel] = Nil + private def panels = _panels + private def panels_= (panels: List[Mutator_Panel]) { + _panels = panels + paintPanels + } + + container.events += { + case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m)) + case Mutator_Event.NewList(ms) => panels = getPanels(ms) + } + + override def open() { + if (!visible) + panels = getPanels(container()) + + super.open + } + + minimumSize = new Dimension(700, 200) + preferredSize = new Dimension(1000, 300) + peer.setFocusTraversalPolicy(focusTraversal) + + private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] = + m.filter(_ match {case (_, _, Identity()) => false; case _ => true}) + .map(m => new Mutator_Panel(m)) + + private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = + panels.map(panel => panel.get_Mutator_Markup) + + private def movePanelUp(m: Mutator_Panel) = { + def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { + case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) + case _ => l + } + + panels = moveUp(panels) + } + + private def movePanelDown(m: Mutator_Panel) = { + def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { + case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) + case _ => l + } + + panels = moveDown(panels) + } + + private def removePanel(m: Mutator_Panel) = { + panels = panels.filter(_ != m).toList + } + + private def addPanel(m: Mutator_Panel) = { + panels = panels ::: List(m) + } + + def paintPanels = { + focusTraversal.clear + filterPanel.contents.clear + panels.map(x => { + filterPanel.contents += x + focusTraversal.addAll(x.focusList) + }) + filterPanel.contents += Swing.VGlue + + focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component]) + focusTraversal.add(addButton.peer) + focusTraversal.add(applyButton.peer) + focusTraversal.add(cancelButton.peer) + filterPanel.revalidate + filterPanel.repaint + } + + val filterPanel = new BoxPanel(Orientation.Vertical) {} + + private val mutatorBox = new ComboBox[Mutator](container.available) + + private val addButton: Button = new Button{ + action = Action("Add") { + addPanel( + new Mutator_Panel((true, visualizer.Colors.next, + mutatorBox.selection.item)) + ) + } + } + + private val applyButton = new Button{ + action = Action("Apply") { + container(getMutators(panels)) + } + } + + private val resetButton = new Button { + action = Action("Reset") { + panels = getPanels(container()) + } + } + + private val cancelButton = new Button{ + action = Action("Close") { + close + } + } + defaultButton = cancelButton + + private val botPanel = new BoxPanel(Orientation.Horizontal) { + border = new EmptyBorder(10, 0, 0, 0) + + contents += mutatorBox + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += addButton + + contents += Swing.HGlue + contents += Swing.RigidBox(new Dimension(30, 0)) + contents += applyButton + + contents += Swing.RigidBox(new Dimension(5, 0)) + contents += resetButton + + contents += Swing.RigidBox(new Dimension(5, 0)) + contents += cancelButton + } + + contents = new BorderPanel { + border = new EmptyBorder(5, 5, 5, 5) + + add(new ScrollPane(filterPanel), BorderPanel.Position.Center) + add(botPanel, BorderPanel.Position.South) + } + + private class Mutator_Panel(initials: Mutator_Markup) + extends BoxPanel(Orientation.Horizontal) + { + private val (_enabled, _color, _mutator) = initials + + private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs() + var focusList = List.empty[java.awt.Component] + private val enabledBox = new iCheckBox("Enabled", _enabled) + + border = new EmptyBorder(5, 5, 5, 5) + maximumSize = new Dimension(Integer.MAX_VALUE, 30) + background = _color + + contents += new Label(_mutator.name) { + preferredSize = new Dimension(175, 20) + horizontalAlignment = Alignment.Left + if (_mutator.description != "") tooltip = _mutator.description + } + contents += Swing.RigidBox(new Dimension(10, 0)) + contents += enabledBox + contents += Swing.RigidBox(new Dimension(5, 0)) + focusList = enabledBox.peer :: focusList + inputs.map( _ match { + case (n, c) => { + contents += Swing.RigidBox(new Dimension(10, 0)) + if (n != "") { + contents += new Label(n) + contents += Swing.RigidBox(new Dimension(5, 0)) + } + contents += c.asInstanceOf[Component] + + focusList = c.asInstanceOf[Component].peer :: focusList + } + case _ => + }) + + { + val t = this + contents += Swing.HGlue + contents += Swing.RigidBox(new Dimension(10, 0)) + + if (show_color_chooser) { + contents += new Button { + maximumSize = new Dimension(20, 20) + + action = Action("Color") { + t.background = + JColorChooser.showDialog(t.peer, "Choose new Color", t.background) + } + + focusList = this.peer :: focusList + } + contents += Swing.RigidBox(new Dimension(2, 0)) + } + + contents += new Button { + maximumSize = new Dimension(20, 20) + + action = Action("Up") { + movePanelUp(t) + } + + focusList = this.peer :: focusList + } + contents += Swing.RigidBox(new Dimension(2, 0)) + contents += new Button { + maximumSize = new Dimension(20, 20) + + action = Action("Down") { + movePanelDown(t) + } + + focusList = this.peer :: focusList + } + contents += Swing.RigidBox(new Dimension(2, 0)) + contents += new Button { + maximumSize = new Dimension(20, 20) + + action = Action("Del") { + removePanel(t) + } + + focusList = this.peer :: focusList + } + } + + focusList = focusList.reverse + + private def isRegex(regex: String): Boolean = { + try { + regex.r + + true + } catch { + case _: java.util.regex.PatternSyntaxException => false + } + } + + def get_Mutator_Markup: Mutator_Markup = { + def regexOrElse(regex: String, orElse: String): String = { + if (isRegex(regex)) regex + else orElse + } + + val m = _mutator match { + case Identity() => + Identity() + case Node_Expression(r, _, _, _) => + Node_Expression( + regexOrElse(inputs(2)._2.getString, r), + inputs(3)._2.getBool, + // "Parents" means "Show parents" or "Matching Children" + inputs(1)._2.getBool, + inputs(0)._2.getBool + ) + case Node_List(_, _, _, _) => + Node_List( + inputs(2)._2.getString.split(',').filter(_ != "").toList, + inputs(3)._2.getBool, + // "Parents" means "Show parents" or "Matching Children" + inputs(1)._2.getBool, + inputs(0)._2.getBool + ) + case Edge_Endpoints(_, _) => + Edge_Endpoints( + inputs(0)._2.getString, + inputs(1)._2.getString + ) + case Add_Node_Expression(r) => + Add_Node_Expression( + regexOrElse(inputs(0)._2.getString, r) + ) + case Add_Transitive_Closure(_, _) => + Add_Transitive_Closure( + inputs(0)._2.getBool, + inputs(1)._2.getBool + ) + case _ => + Identity() + } + + (enabledBox.selected, background, m) + } + + private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match { + case Node_Expression(regex, reverse, check_parents, check_children) => + List( + ("", new iCheckBox("Parents", check_children)), + ("", new iCheckBox("Children", check_parents)), + ("Regex", new iTextField(regex, x => !isRegex(x))), + ("", new iCheckBox(reverse_caption, reverse)) + ) + case Node_List(list, reverse, check_parents, check_children) => + List( + ("", new iCheckBox("Parents", check_children)), + ("", new iCheckBox("Children", check_parents)), + ("Names", new iTextField(list.mkString(","))), + ("", new iCheckBox(reverse_caption, reverse)) + ) + case Edge_Endpoints(source, dest) => + List( + ("Source", new iTextField(source)), + ("Destination", new iTextField(dest)) + ) + case Add_Node_Expression(regex) => + List( + ("Regex", new iTextField(regex, x => !isRegex(x))) + ) + case Add_Transitive_Closure(parents, children) => + List( + ("", new iCheckBox("Parents", parents)), + ("", new iCheckBox("Children", children)) + ) + case _ => Nil + } + } + + private trait Mutator_Input_Value + { + def getString: String + def getBool: Boolean + } + + private class iTextField(t: String, colorator: String => Boolean) + extends TextField(t) with Mutator_Input_Value + { + def this(t: String) = this(t, x => false) + + preferredSize = new Dimension(125, 18) + + reactions += { + case ValueChanged(_) => + if (colorator(text)) + background = Color.RED + else + background = Color.WHITE + } + + def getString = text + def getBool = true + } + + private class iCheckBox(t: String, s: Boolean) + extends CheckBox(t) with Mutator_Input_Value + { + selected = s + + def getString = "" + def getBool = selected + } + + private object focusTraversal + extends FocusTraversalPolicy + { + private var items = Vector[java.awt.Component]() + + def add(c: java.awt.Component) { + items = items :+ c + } + def addAll(cs: TraversableOnce[java.awt.Component]) { + items = items ++ cs + } + def clear() { + items = Vector[java.awt.Component]() + } + + def getComponentAfter(root: java.awt.Container, + c: java.awt.Component): java.awt.Component = { + val i = items.indexOf(c) + if (i < 0) { + getDefaultComponent(root) + } else { + items((i + 1) % items.length) + } + } + + def getComponentBefore(root: java.awt.Container, + c: java.awt.Component): java.awt.Component = { + val i = items.indexOf(c) + if (i < 0) { + getDefaultComponent(root) + } else { + items((i - 1) % items.length) + } + } + + def getFirstComponent(root: java.awt.Container): java.awt.Component = { + if (items.length > 0) + items(0) + else + null + } + + def getDefaultComponent(root: java.awt.Container) + : java.awt.Component = getFirstComponent(root) + + def getLastComponent(root: java.awt.Container): java.awt.Component = { + if (items.length > 0) + items.last + else + null + } + } +} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/mutator_event.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/mutator_event.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,35 @@ +/* Title: Tools/Graphview/mutator_event.scala + Author: Markus Kaiser, TU Muenchen + +Events for dialog synchronization. +*/ + +package isabelle.graphview + + +import isabelle._ + +import scala.collection.mutable + +import java.awt.Color + + +object Mutator_Event +{ + type Mutator_Markup = (Boolean, Color, Mutator) + + sealed abstract class Message + case class Add(m: Mutator_Markup) extends Message + case class NewList(m: List[Mutator_Markup]) extends Message + + type Receiver = PartialFunction[Message, Unit] + + class Bus + { + private val receivers = new mutable.ListBuffer[Receiver] + + def += (r: Receiver) { GUI_Thread.require {}; receivers += r } + def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } + def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } + } +} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/popups.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/popups.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,176 @@ +/* Title: Tools/Graphview/popups.scala + Author: Markus Kaiser, TU Muenchen + +PopupMenu generation for graph components. +*/ + +package isabelle.graphview + + +import isabelle._ +import isabelle.graphview.Mutators._ + +import javax.swing.JPopupMenu +import scala.swing.{Action, Menu, MenuItem, Separator} + + +object Popups +{ + def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]) + : JPopupMenu = + { + val visualizer = panel.visualizer + + val add_mutator = visualizer.model.Mutators.add _ + val curr = visualizer.model.current + + def filter_context(ls: List[String], reverse: Boolean, + caption: String, edges: Boolean) = + new Menu(caption) { + contents += new MenuItem(new Action("This") { + def apply = + add_mutator( + Mutators.create(visualizer, + Node_List(ls, reverse, false, false) + ) + ) + }) + + contents += new MenuItem(new Action("Family") { + def apply = + add_mutator( + Mutators.create(visualizer, + Node_List(ls, reverse, true, true) + ) + ) + }) + + contents += new MenuItem(new Action("Parents") { + def apply = + add_mutator( + Mutators.create(visualizer, + Node_List(ls, reverse, false, true) + ) + ) + }) + + contents += new MenuItem(new Action("Children") { + def apply = + add_mutator( + Mutators.create(visualizer, + Node_List(ls, reverse, true, false) + ) + ) + }) + + + if (edges) { + val outs = ls.map(l => (l, curr.imm_succs(l))) // FIXME iterator + .filter(_._2.size > 0).sortBy(_._1) + val ins = ls.map(l => (l, curr.imm_preds(l))) // FIXME iterator + .filter(_._2.size > 0).sortBy(_._1) + + if (outs.nonEmpty || ins.nonEmpty) { + contents += new Separator() + + contents += new Menu("Edge") { + if (outs.nonEmpty) { + contents += new MenuItem("From...") { + enabled = false + } + + outs.map( e => { + val (from, tos) = e + contents += new Menu(from) { + contents += new MenuItem("To..."){ + enabled = false + } + + tos.toList.sorted.distinct.map( to => { + contents += new MenuItem(new Action(to) { + def apply = + add_mutator( + Mutators.create(visualizer, Edge_Endpoints(from, to)) + ) + }) + }) + } + }) + } + if (outs.nonEmpty && ins.nonEmpty) { + contents += new Separator() + } + if (ins.nonEmpty) { + contents += new MenuItem("To...") { + enabled = false + } + + ins.map( e => { + val (to, froms) = e + contents += new Menu(to) { + contents += new MenuItem("From..."){ + enabled = false + } + + froms.toList.sorted.distinct.map( from => { + contents += new MenuItem(new Action(from) { + def apply = + add_mutator( + Mutators.create(visualizer, Edge_Endpoints(from, to)) + ) + }) + }) + } + }) + } + } + } + } + } + + val popup = new JPopupMenu() + + popup.add(new MenuItem(new Action("Remove all filters") { + def apply = visualizer.model.Mutators(Nil) + }).peer + ) + popup.add(new JPopupMenu.Separator) + + if (under_mouse.isDefined) { + val v = under_mouse.get + popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) { + enabled = false + }.peer) + + popup.add(filter_context(List(v), true, "Hide", true).peer) + popup.add(filter_context(List(v), false, "Show only", false).peer) + + popup.add(new JPopupMenu.Separator) + } + if (!selected.isEmpty) { + val text = { + if (selected.length > 1) { + "Multiple" + } else { + visualizer.Caption(selected.head) + } + } + + popup.add(new MenuItem("Selected: %s".format(text)) { + enabled = false + }.peer) + + popup.add(filter_context(selected, true, "Hide", true).peer) + popup.add(filter_context(selected, false, "Show only", false).peer) + popup.add(new JPopupMenu.Separator) + } + + + popup.add(new MenuItem(new Action("Fit to Window") { + def apply = panel.fit_to_window() + }).peer + ) + + popup + } +} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/shapes.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/shapes.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,255 @@ +/* Title: Tools/Graphview/shapes.scala + Author: Markus Kaiser, TU Muenchen + +Drawable shapes. +*/ + +package isabelle.graphview + + +import java.awt.{BasicStroke, Graphics2D, Shape} +import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator} + + +object Shapes +{ + trait Node + { + def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape + def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit + } + + object Growing_Node extends Node + { + private val stroke = + new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) + + def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double = + { + val (x, y) = visualizer.Coordinates(peer.get) + val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g) + val w = bounds.getWidth + visualizer.pad_x + val h = bounds.getHeight + visualizer.pad_y + new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h) + } + + def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) + { + val caption = visualizer.Caption(peer.get) + val bounds = g.getFontMetrics.getStringBounds(caption, g) + val s = shape(g, visualizer, peer) + + val (border, background, foreground) = visualizer.Color(peer) + g.setStroke(stroke) + g.setColor(border) + g.draw(s) + g.setColor(background) + g.fill(s) + g.setColor(foreground) + g.drawString(caption, + (s.getCenterX + (- bounds.getWidth / 2)).toFloat, + (s.getCenterY + 5).toFloat) + } + } + + object Dummy extends Node + { + private val stroke = + new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) + private val shape = new Rectangle2D.Double(-5, -5, 10, 10) + private val identity = new AffineTransform() + + def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape + + def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit = + paint_transformed(g, visualizer, peer, identity) + + def paint_transformed(g: Graphics2D, visualizer: Visualizer, + peer: Option[String], at: AffineTransform) + { + val (border, background, foreground) = visualizer.Color(peer) + g.setStroke(stroke) + g.setColor(border) + g.draw(at.createTransformedShape(shape)) + } + } + + trait Edge + { + def paint(g: Graphics2D, visualizer: Visualizer, + peer: (String, String), head: Boolean, dummies: Boolean) + } + + object Straight_Edge extends Edge + { + private val stroke = + new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) + + def paint(g: Graphics2D, visualizer: Visualizer, + peer: (String, String), head: Boolean, dummies: Boolean) + { + val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) + val ds = + { + val min = fy min ty + val max = fy max ty + visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max }) + } + val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) + + path.moveTo(fx, fy) + ds.foreach({case (x, y) => path.lineTo(x, y)}) + path.lineTo(tx, ty) + + if (dummies) { + ds.foreach({ + case (x, y) => { + val at = AffineTransform.getTranslateInstance(x, y) + Dummy.paint_transformed(g, visualizer, None, at) + } + }) + } + + g.setStroke(stroke) + g.setColor(visualizer.Color(peer)) + g.draw(path) + + if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) + } + } + + object Cardinal_Spline_Edge extends Edge + { + private val stroke = + new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) + private val slack = 0.1 + + def paint(g: Graphics2D, visualizer: Visualizer, + peer: (String, String), head: Boolean, dummies: Boolean) + { + val ((fx, fy), (tx, ty)) = + (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) + val ds = + { + val min = fy min ty + val max = fy max ty + visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max}) + } + + if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies) + else { + val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) + path.moveTo(fx, fy) + + val coords = ((fx, fy) :: ds ::: List((tx, ty))) + val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2) + + val (dx2, dy2) = + ((dx, dy) /: coords.sliding(3))({ + case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => { + val (dx2, dy2) = (rx - lx, ry - ly) + + path.curveTo(lx + slack * dx , ly + slack * dy, + mx - slack * dx2, my - slack * dy2, + mx , my) + (dx2, dy2) + } + }) + + val (lx, ly) = ds.last + path.curveTo(lx + slack * dx2, ly + slack * dy2, + tx - slack * dx2, ty - slack * dy2, + tx , ty) + + if (dummies) { + ds.foreach({ + case (x, y) => { + val at = AffineTransform.getTranslateInstance(x, y) + Dummy.paint_transformed(g, visualizer, None, at) + } + }) + } + + g.setStroke(stroke) + g.setColor(visualizer.Color(peer)) + g.draw(path) + + if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) + } + } + } + + object Arrow_Head + { + type Point = (Double, Double) + + private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = + { + def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = + { + val i = path.getPathIterator(null, 1.0) + val seg = Array[Double](0,0,0,0,0,0) + var p1 = (0.0, 0.0) + var p2 = (0.0, 0.0) + while (!i.isDone()) { + i.currentSegment(seg) match { + case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) + case PathIterator.SEG_LINETO => + p1 = p2 + p2 = (seg(0), seg(1)) + + if(shape.contains(seg(0), seg(1))) + return Some((p1, p2)) + case _ => + } + i.next() + } + None + } + + def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = + { + val ((fx, fy), (tx, ty)) = line + if (shape.contains(fx, fy) == shape.contains(tx, ty)) + None + else { + val (dx, dy) = (fx - tx, fy - ty) + if ((dx * dx + dy * dy) < 1.0) { + val at = AffineTransform.getTranslateInstance(fx, fy) + at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) + Some(at) + } + else { + val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) + if (shape.contains(fx, fy) == shape.contains(mx, my)) + binary_search(((mx, my), (tx, ty)), shape) + else + binary_search(((fx, fy), (mx, my)), shape) + } + } + } + + intersecting_line(path, shape) match { + case None => None + case Some(line) => binary_search(line, shape) + } + } + + def paint(g: Graphics2D, path: GeneralPath, shape: Shape) + { + position(path, shape) match { + case None => + case Some(at) => + val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) + arrow.moveTo(0, 0) + arrow.lineTo(-10, 4) + arrow.lineTo(-6, 0) + arrow.lineTo(-10, -4) + arrow.lineTo(0, 0) + arrow.transform(at) + + g.fill(arrow) + } + } + } +} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/graph_panel.scala --- a/src/Tools/Graphview/src/graph_panel.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,298 +0,0 @@ -/* Title: Tools/Graphview/src/graph_panel.scala - Author: Markus Kaiser, TU Muenchen - -Graphview Java2D drawing panel. -*/ - -package isabelle.graphview - - -import isabelle._ - -import java.awt.{Dimension, Graphics2D, Point, Rectangle} -import java.awt.geom.{AffineTransform, Point2D} -import java.awt.image.BufferedImage -import javax.swing.{JScrollPane, JComponent} - -import scala.swing.{Panel, ScrollPane} -import scala.swing.event._ - - -class Graph_Panel( - val visualizer: Visualizer, - make_tooltip: (JComponent, Int, Int, XML.Body) => String) - extends ScrollPane -{ - panel => - - tooltip = "" - - override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { - 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 { - case Nil => null - case content => make_tooltip(panel.peer, event.getX, event.getY, content) - } - case None => null - } - } - - peer.setWheelScrollingEnabled(false) - focusable = true - requestFocus() - - horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always - verticalScrollBarPolicy = ScrollPane.BarPolicy.Always - - def node(at: Point2D): Option[String] = - visualizer.model.visible_nodes_iterator - .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at)) - - def refresh() - { - if (paint_panel != null) { - paint_panel.set_preferred_size() - paint_panel.repaint() - } - } - - def fit_to_window() = { - Transform.fit_to_window() - refresh() - } - - val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) } - - def rescale(s: Double) - { - Transform.scale = s - if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt) - refresh() - } - - def apply_layout() = visualizer.Coordinates.update_layout() - - private class Paint_Panel extends Panel { - def set_preferred_size() { - val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() - val s = Transform.scale_discrete - val (px, py) = Transform.padding - - preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt, - (math.abs(maxY - minY + py) * s).toInt) - - revalidate() - } - - override def paint(g: Graphics2D) { - super.paintComponent(g) - g.transform(Transform()) - - visualizer.Drawer.paint_all_visible(g, true) - } - } - private val paint_panel = new Paint_Panel - contents = paint_panel - - listenTo(keys) - listenTo(mouse.moves) - listenTo(mouse.clicks) - listenTo(mouse.wheel) - reactions += Interaction.Mouse.react - reactions += Interaction.Keyboard.react - reactions += { - case KeyTyped(_, _, _, _) => {repaint(); requestFocus()} - case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()} - case MouseDragged(_, _, _) => {repaint(); requestFocus()} - case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()} - case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()} - case MouseMoved(_, _, _) => repaint() - } - - visualizer.model.Colors.events += { case _ => repaint() } - visualizer.model.Mutators.events += { case _ => repaint() } - - apply_layout() - rescale(1.0) - - private object Transform - { - val padding = (100, 40) - - private var _scale: Double = 1.0 - def scale: Double = _scale - def scale_=(s: Double) - { - _scale = (s min 10) max 0.1 - } - def scale_discrete: Double = - (_scale * visualizer.font_size).round.toDouble / visualizer.font_size - - def apply() = { - val (minX, minY, _, _) = visualizer.Coordinates.bounds() - - val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete) - at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2) - at - } - - def fit_to_window() { - if (visualizer.model.visible_nodes_iterator.isEmpty) - rescale(1.0) - else { - val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds() - - val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2) - val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy) - rescale(sx min sy) - } - } - - def pane_to_graph_coordinates(at: Point2D): Point2D = { - val s = Transform.scale_discrete - val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null) - - p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s) - p - } - } - - object Interaction { - object Keyboard { - import scala.swing.event.Key._ - - val react: PartialFunction[Event, Unit] = { - case KeyTyped(_, c, m, _) => typed(c, m) - } - - def typed(c: Char, m: Modifiers) = - (c, m) match { - case ('+', _) => rescale(Transform.scale * 5.0/4) - case ('-', _) => rescale(Transform.scale * 4.0/5) - case ('0', _) => Transform.fit_to_window() - case ('1', _) => visualizer.Coordinates.update_layout() - case ('2', _) => Transform.fit_to_window() - case _ => - } - } - - object Mouse { - import scala.swing.event.Key.Modifier._ - type Modifiers = Int - type Dummy = ((String, String), Int) - - private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null - - val react: PartialFunction[Event, Unit] = { - case MousePressed(_, p, _, _, _) => pressed(p) - case MouseDragged(_, to, _) => { - drag(draginfo, to) - val (_, p, d) = draginfo - draginfo = (to, p, d) - } - case MouseWheelMoved(_, p, _, r) => wheel(r, p) - case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e) - } - - def dummy(at: Point2D): Option[Dummy] = - visualizer.model.visible_edges_iterator.map({ - i => visualizer.Coordinates(i).zipWithIndex.map((i, _)) - }).flatten.find({ - case (_, ((x, y), _)) => - visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y) - }) match { - case None => None - case Some((name, (_, index))) => Some((name, index)) - } - - def pressed(at: Point) { - val c = Transform.pane_to_graph_coordinates(at) - val l = node(c) match { - case Some(l) => - if (visualizer.Selection(l)) visualizer.Selection() else List(l) - case None => Nil - } - val d = l match { - case Nil => dummy(c) match { - case Some(d) => List(d) - case None => Nil - } - - case _ => Nil - } - - draginfo = (at, l, d) - } - - def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) { - import javax.swing.SwingUtilities - - val c = Transform.pane_to_graph_coordinates(at) - val p = node(c) - - def left_click() { - (p, m) match { - case (Some(l), Control) => visualizer.Selection.add(l) - case (None, Control) => - - case (Some(l), Shift) => visualizer.Selection.add(l) - case (None, Shift) => - - case (Some(l), _) => visualizer.Selection.set(List(l)) - case (None, _) => visualizer.Selection.clear - } - } - - def right_click() { - val menu = Popups(panel, p, visualizer.Selection()) - menu.show(panel.peer, at.x, at.y) - } - - if (clicks < 2) { - if (SwingUtilities.isRightMouseButton(e.peer)) right_click() - else left_click() - } - } - - def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) { - val (from, p, d) = draginfo - - val s = Transform.scale_discrete - val (dx, dy) = (to.x - from.x, to.y - from.y) - (p, d) match { - case (Nil, Nil) => { - val r = panel.peer.getViewport.getViewRect - r.translate(-dx, -dy) - - paint_panel.peer.scrollRectToVisible(r) - } - - case (Nil, ds) => - ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s))) - - case (ls, _) => - ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s))) - } - } - - def wheel(rotation: Int, at: Point) { - val at2 = Transform.pane_to_graph_coordinates(at) - // > 0 -> up - rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4)) - - // move mouseposition to center - Transform().transform(at2, at2) - val r = panel.peer.getViewport.getViewRect - val (width, height) = (r.getWidth, r.getHeight) - paint_panel.peer.scrollRectToVisible( - new Rectangle((at2.getX() - width / 2).toInt, - (at2.getY() - height / 2).toInt, - width.toInt, - height.toInt) - ) - } - } - } -} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/layout_pendulum.scala --- a/src/Tools/Graphview/src/layout_pendulum.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,275 +0,0 @@ -/* Title: Tools/Graphview/src/layout_pendulum.scala - Author: Markus Kaiser, TU Muenchen - -Pendulum DAG layout algorithm. -*/ - -package isabelle.graphview - - -import isabelle._ - - -object Layout_Pendulum -{ - type Key = String - type Point = (Double, Double) - type Coordinates = Map[Key, Point] - type Level = List[Key] - type Levels = List[Level] - type Dummies = (Model.Graph, List[Key], Map[Key, Int]) - - case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]]) - val empty_layout = Layout(Map.empty, Map.empty) - - val pendulum_iterations = 10 - val minimize_crossings_iterations = 40 - - def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = - { - if (graph.is_empty) empty_layout - else { - val initial_levels = level_map(graph) - - val (dummy_graph, dummies, dummy_levels) = - ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { - case ((graph, dummies, levels), from) => - ((graph, dummies, levels) /: graph.imm_succs(from)) { - case ((graph, dummies, levels), to) => - if (levels(to) - levels(from) <= 1) (graph, dummies, levels) - else { - val (next, ds, ls) = add_dummies(graph, from, to, levels) - (next, dummies + ((from, to) -> ds), ls) - } - } - } - - val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) - - val initial_coordinates: Coordinates = - (((Map.empty[Key, Point], 0.0) /: levels) { - case ((coords1, y), level) => - ((((coords1, 0.0) /: level) { - case ((coords2, x), key) => - val s = if (graph.defined(key)) graph.get_node(key).name else "X" - (coords2 + (key -> (x, y)), x + box_distance) - })._1, y + box_height(level.length)) - })._1 - - val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) - - val dummy_coords = - (Map.empty[(Key, Key), List[Point]] /: dummies.keys) { - case (map, key) => map + (key -> dummies(key).map(coords(_))) - } - - Layout(coords, dummy_coords) - } - } - - - def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = - { - val ds = - ((levels(from) + 1) until levels(to)) - .map("%s$%s$%d" format (from, to, _)).toList - - val ls = - (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { - case (ls, (l, d)) => ls + (d -> l) - } - - val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) - val graph2 = - (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { - case (g, List(x, y)) => g.add_edge(x, y) - } - (graph2, ds, ls) - } - - def level_map(graph: Model.Graph): Map[Key, Int] = - (Map.empty[Key, Int] /: graph.topological_order) { - (levels, key) => { - val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) } - levels + (key -> lev) - } - } - - def level_list(map: Map[Key, Int]): Levels = - { - val max_lev = (-1 /: map) { case (m, (_, l)) => m max l } - val buckets = new Array[Level](max_lev + 1) - for (l <- 0 to max_lev) { buckets(l) = Nil } - for ((key, l) <- map) { buckets(l) = key :: buckets(l) } - buckets.iterator.map(_.sorted).toList - } - - def count_crossings(graph: Model.Graph, levels: Levels): Int = - { - def in_level(ls: Levels): Int = ls match { - case List(top, bot) => - top.iterator.zipWithIndex.map { - case (outer_parent, outer_parent_index) => - graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) - .map(outer_child => - (0 until outer_parent_index) - .map(inner_parent => - graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) - .filter(inner_child => outer_child < inner_child) - .size - ).sum - ).sum - }.sum - - case _ => 0 - } - - levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum - } - - def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = - { - def resort_level(parent: Level, child: Level, top_down: Boolean): Level = - child.map(k => { - val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) - val weight = - (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) - (k, weight) - }).sortBy(_._2).map(_._1) - - def resort(levels: Levels, top_down: Boolean) = top_down match { - case true => - (List[Level](levels.head) /: levels.tail) { - (tops, bot) => resort_level(tops.head, bot, top_down) :: tops - }.reverse - - case false => - (List[Level](levels.reverse.head) /: levels.reverse.tail) { - (bots, top) => resort_level(bots.head, top, top_down) :: bots - } - } - - ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { - case ((old_levels, old_crossings, top_down), _) => { - val new_levels = resort(old_levels, top_down) - val new_crossings = count_crossings(graph, new_levels) - if (new_crossings < old_crossings) - (new_levels, new_crossings, !top_down) - else - (old_levels, old_crossings, !top_down) - } - }._1 - } - - def pendulum(graph: Model.Graph, box_distance: Double, - levels: Levels, coords: Map[Key, Point]): Coordinates = - { - type Regions = List[List[Region]] - - def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) - : (Regions, Coordinates, Boolean) = - { - val (nextr, nextc, moved) = - ((List.empty[List[Region]], coords, false) /: - (if (top_down) regions else regions.reverse)) { - case ((tops, coords, prev_moved), bot) => { - val nextb = collapse(coords, bot, top_down) - val (nextc, this_moved) = deflect(coords, nextb, top_down) - (nextb :: tops, nextc, prev_moved || this_moved) - } - } - - (nextr.reverse, nextc, moved) - } - - def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = - { - if (level.size <= 1) level - else { - var next = level - var regions_changed = true - while (regions_changed) { - regions_changed = false - for (i <- (next.length to 1)) { - val (r1, r2) = (next(i-1), next(i)) - val d1 = r1.deflection(coords, top_down) - val d2 = r2.deflection(coords, top_down) - - if (// Do regions touch? - r1.distance(coords, r2) <= box_distance && - // Do they influence each other? - (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) - { - regions_changed = true - r1.nodes = r1.nodes ::: r2.nodes - next = next.filter(next.indexOf(_) != i) - } - } - } - next - } - } - - def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) - : (Coordinates, Boolean) = - { - ((coords, false) /: (0 until level.length)) { - case ((coords, moved), i) => { - val r = level(i) - val d = r.deflection(coords, top_down) - val offset = { - if (i == 0 && d <= 0) d - else if (i == level.length - 1 && d >= 0) d - else if (d < 0) { - val prev = level(i-1) - (-(r.distance(coords, prev) - box_distance)) max d - } - else { - val next = level(i+1) - (r.distance(coords, next) - box_distance) min d - } - } - - (r.move(coords, offset), moved || (d != 0)) - } - } - } - - val regions = levels.map(level => level.map(new Region(graph, _))) - - ((regions, coords, true, true) /: (1 to pendulum_iterations)) { - case ((regions, coords, top_down, moved), _) => - if (moved) { - val (nextr, nextc, m) = iteration(regions, coords, top_down) - (nextr, nextc, !top_down, m) - } - else (regions, coords, !top_down, moved) - }._2 - } - - private class Region(val graph: Model.Graph, node: Key) - { - var nodes: List[Key] = List(node) - - def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min - def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max - - def distance(coords: Coordinates, to: Region): Double = - math.abs(left(coords) - to.left(coords)) min - math.abs(right(coords) - to.right(coords)) - - def deflection(coords: Coordinates, use_preds: Boolean) = - nodes.map(k => (coords(k)._1, - if (use_preds) graph.imm_preds(k).toList // FIXME iterator - else graph.imm_succs(k).toList)) - .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) }) - .sum / nodes.length - - def move(coords: Coordinates, by: Double): Coordinates = - (coords /: nodes) { - case (cs, node) => - val (x, y) = cs(node) - cs + (node -> (x + by, y)) - } - } -} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/main_panel.scala --- a/src/Tools/Graphview/src/main_panel.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -/* Title: Tools/Graphview/src/main_panel.scala - Author: Markus Kaiser, TU Muenchen - -Graph Panel wrapper. -*/ - -package isabelle.graphview - - -import isabelle._ -import isabelle.graphview.Mutators._ - -import scala.collection.JavaConversions._ -import scala.swing.{BorderPanel, Button, BoxPanel, - Orientation, Swing, CheckBox, Action, FileChooser} - -import java.io.{File => JFile} -import java.awt.{Color, Dimension, Graphics2D} -import java.awt.geom.Rectangle2D -import java.awt.image.BufferedImage -import javax.imageio.ImageIO -import javax.swing.border.EmptyBorder -import javax.swing.JComponent - - -class Main_Panel(graph: Model.Graph) 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) - - listenTo(keys) - reactions += graph_panel.reactions - - val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false) - - val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations") - - private val chooser = new FileChooser() - chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly - chooser.title = "Save Image (.png or .pdf)" - - val options_panel = new BoxPanel(Orientation.Horizontal) { - border = new EmptyBorder(0, 0, 10, 0) - - contents += Swing.HGlue - contents += new CheckBox(){ - selected = visualizer.arrow_heads - action = Action("Arrow Heads"){ - visualizer.arrow_heads = selected - graph_panel.repaint() - } - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Button{ - action = Action("Save Image"){ - chooser.showSaveDialog(this) match { - case FileChooser.Result.Approve => export(chooser.selectedFile) - case _ => - } - } - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += graph_panel.zoom - - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Button{ - action = Action("Apply Layout"){ - graph_panel.apply_layout() - } - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Button{ - action = Action("Fit to Window"){ - graph_panel.fit_to_window() - } - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Button{ - action = Action("Colorations"){ - color_dialog.open - } - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Button{ - action = Action("Filters"){ - mutator_dialog.open - } - } - } - - add(graph_panel, BorderPanel.Position.Center) - add(options_panel, BorderPanel.Position.North) - - private def export(file: JFile) - { - val (x0, y0, x1, y1) = visualizer.Coordinates.bounds - val w = (math.abs(x1 - x0) + 400).toInt - val h = (math.abs(y1 - y0) + 200).toInt - - def paint(gfx: Graphics2D) - { - gfx.setColor(Color.WHITE) - gfx.fill(new Rectangle2D.Double(0, 0, w, h)) - - gfx.translate(- x0 + 200, - y0 + 100) - visualizer.Drawer.paint_all_visible(gfx, false) - } - - try { - val name = file.getName - if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h) - else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h) - else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)") - } - catch { - case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg)) - } - } -} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/model.scala --- a/src/Tools/Graphview/src/model.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -/* Title: Tools/Graphview/src/model.scala - Author: Markus Kaiser, TU Muenchen - -Internal graph representation. -*/ - -package isabelle.graphview - - -import isabelle._ -import isabelle.graphview.Mutators._ - -import java.awt.Color - - -class Mutator_Container(val available: List[Mutator]) { - type Mutator_Markup = (Boolean, Color, Mutator) - - val events = new Mutator_Event.Bus - - private var _mutators : List[Mutator_Markup] = Nil - def apply() = _mutators - def apply(mutators: List[Mutator_Markup]){ - _mutators = mutators - - events.event(Mutator_Event.NewList(mutators)) - } - - def add(mutator: Mutator_Markup) = { - _mutators = _mutators ::: List(mutator) - - events.event(Mutator_Event.Add(mutator)) - } -} - - -object Model -{ - /* node info */ - - sealed case class Info(name: String, content: XML.Body) - - val empty_info: Info = Info("", Nil) - - val decode_info: XML.Decode.T[Info] = (body: XML.Body) => - { - import XML.Decode._ - - val (name, content) = pair(string, x => x)(body) - Info(name, content) - } - - - /* graph */ - - type Graph = isabelle.Graph[String, Info] - - val decode_graph: XML.Decode.T[Graph] = - isabelle.Graph.decode(XML.Decode.string, decode_info) -} - -class Model(private val graph: Model.Graph) { - val Mutators = new Mutator_Container( - List( - Node_Expression(".*", false, false, false), - Node_List(Nil, false, false, false), - Edge_Endpoints("", ""), - Add_Node_Expression(""), - Add_Transitive_Closure(true, true) - )) - - val Colors = new Mutator_Container( - List( - Node_Expression(".*", false, false, false), - Node_List(Nil, false, false, false) - )) - - def visible_nodes_iterator: Iterator[String] = current.keys_iterator - - def visible_edges_iterator: Iterator[(String, String)] = - current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _))) - - def complete = graph - def current: Model.Graph = - (graph /: Mutators()) { - case (g, (enabled, _, mutator)) => { - if (!enabled) g - else mutator.mutate(graph, g) - } - } - - private var _colors = Map.empty[String, Color] - def colors = _colors - - private def build_colors() { - _colors = - (Map.empty[String, Color] /: Colors()) ({ - case (colors, (enabled, color, mutator)) => { - (colors /: mutator.mutate(graph, graph).keys_iterator) ({ - case (colors, k) => colors + (k -> color) - }) - } - }) - } - Colors.events += { case _ => build_colors() } -} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/mutator.scala --- a/src/Tools/Graphview/src/mutator.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,199 +0,0 @@ -/* Title: Tools/Graphview/src/mutator.scala - Author: Markus Kaiser, TU Muenchen - -Filters and add-operations on graphs. -*/ - -package isabelle.graphview - - -import isabelle._ - -import java.awt.Color -import scala.collection.immutable.SortedSet - - -trait Mutator -{ - val name: String - val description: String - def mutate(complete: Model.Graph, sub: 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 -} - -object Mutators { - type Mutator_Markup = (Boolean, Color, Mutator) - - val Enabled = true - val Disabled = false - - def create(visualizer: Visualizer, m: Mutator): Mutator_Markup = - (Mutators.Enabled, visualizer.Colors.next, m) - - class Graph_Filter(val name: String, val description: String, - pred: Model.Graph => Model.Graph) - extends Filter - { - def filter(sub: Model.Graph) : Model.Graph = pred(sub) - } - - class Graph_Mutator(val name: String, 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) - } - - class Node_Filter(name: String, description: String, - pred: (Model.Graph, String) => Boolean) - extends Graph_Filter ( - - name, - description, - g => g.restrict(pred(g, _)) - ) - - class Edge_Filter(name: String, description: String, - pred: (Model.Graph, String, String) => Boolean) - extends Graph_Filter ( - - name, - description, - g => (g /: g.dest) { - case (graph, ((from, _), tos)) => { - (graph /: tos) { - (gr, to) => if (pred(gr, from, to)) gr - else gr.del_edge(from, to) - } - } - } - ) - - class Node_Family_Filter(name: String, description: String, - reverse: Boolean, parents: Boolean, children: Boolean, - pred: (Model.Graph, String) => Boolean) - extends Node_Filter( - - name, - description, - (g, k) => reverse != ( - pred(g, k) || - (parents && g.all_preds(List(k)).exists(pred(g, _))) || - (children && g.all_succs(List(k)).exists(pred(g, _))) - ) - ) - - case class Identity() - extends Graph_Filter( - - "Identity", - "Does not change the graph.", - g => g - ) - - case class Node_Expression(regex: String, - reverse: Boolean, parents: Boolean, children: Boolean) - extends Node_Family_Filter( - - "Filter by Name", - "Only shows or hides all nodes with any family member's name matching " + - "a regex.", - reverse, - parents, - children, - (g, k) => (regex.r findFirstIn k).isDefined - ) - - case class Node_List(list: List[String], - reverse: Boolean, parents: Boolean, children: Boolean) - extends Node_Family_Filter( - - "Filter by Name List", - "Only shows or hides all nodes with any family member's name matching " + - "any string in a comma separated list.", - reverse, - parents, - children, - (g, k) => list.exists(_ == k) - ) - - case class Edge_Endpoints(source: String, dest: String) - extends Edge_Filter( - - "Hide edge", - "Hides the edge whose endpoints match strings.", - (g, s, d) => !(s == source && d == dest) - ) - - private def add_node_group(from: Model.Graph, to: Model.Graph, - keys: List[String]) = { - - // Add Nodes - val with_nodes = - (to /: keys) { - (graph, key) => graph.default_node(key, from.get_node(key)) - } - - // Add Edges - (with_nodes /: keys) { - (gv, key) => { - def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) = - (g /: keys) { - (graph, end) => { - if (!graph.keys_iterator.contains(end)) graph - else { - if (succs) graph.add_edge(key, end) - else graph.add_edge(end, key) - } - } - } - - - add_edges( - add_edges(gv, from.imm_preds(key), false), - from.imm_succs(key), true - ) - } - } - } - - case class Add_Node_Expression(regex: String) - extends Graph_Mutator( - - "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) - } - ) - - 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) => { - 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)) - else - withparents - } - ) -} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/mutator_dialog.scala --- a/src/Tools/Graphview/src/mutator_dialog.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,427 +0,0 @@ -/* Title: Tools/Graphview/src/mutator_dialog.scala - Author: Markus Kaiser, TU Muenchen - -Mutator selection and configuration dialog. -*/ - -package isabelle.graphview - - -import isabelle._ - -import java.awt.Color -import java.awt.FocusTraversalPolicy -import javax.swing.JColorChooser -import javax.swing.border.EmptyBorder -import scala.collection.JavaConversions._ -import scala.swing._ -import isabelle.graphview.Mutators._ -import scala.swing.event.ValueChanged - - -class Mutator_Dialog( - visualizer: Visualizer, - container: Mutator_Container, - caption: String, - reverse_caption: String = "Inverse", - show_color_chooser: Boolean = true) - extends Dialog -{ - type Mutator_Markup = (Boolean, Color, Mutator) - - title = caption - - private var _panels: List[Mutator_Panel] = Nil - private def panels = _panels - private def panels_= (panels: List[Mutator_Panel]) { - _panels = panels - paintPanels - } - - container.events += { - case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m)) - case Mutator_Event.NewList(ms) => panels = getPanels(ms) - } - - override def open() { - if (!visible) - panels = getPanels(container()) - - super.open - } - - minimumSize = new Dimension(700, 200) - preferredSize = new Dimension(1000, 300) - peer.setFocusTraversalPolicy(focusTraversal) - - private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] = - m.filter(_ match {case (_, _, Identity()) => false; case _ => true}) - .map(m => new Mutator_Panel(m)) - - private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = - panels.map(panel => panel.get_Mutator_Markup) - - private def movePanelUp(m: Mutator_Panel) = { - def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { - case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs) - case _ => l - } - - panels = moveUp(panels) - } - - private def movePanelDown(m: Mutator_Panel) = { - def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match { - case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs) - case _ => l - } - - panels = moveDown(panels) - } - - private def removePanel(m: Mutator_Panel) = { - panels = panels.filter(_ != m).toList - } - - private def addPanel(m: Mutator_Panel) = { - panels = panels ::: List(m) - } - - def paintPanels = { - focusTraversal.clear - filterPanel.contents.clear - panels.map(x => { - filterPanel.contents += x - focusTraversal.addAll(x.focusList) - }) - filterPanel.contents += Swing.VGlue - - focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component]) - focusTraversal.add(addButton.peer) - focusTraversal.add(applyButton.peer) - focusTraversal.add(cancelButton.peer) - filterPanel.revalidate - filterPanel.repaint - } - - val filterPanel = new BoxPanel(Orientation.Vertical) {} - - private val mutatorBox = new ComboBox[Mutator](container.available) - - private val addButton: Button = new Button{ - action = Action("Add") { - addPanel( - new Mutator_Panel((true, visualizer.Colors.next, - mutatorBox.selection.item)) - ) - } - } - - private val applyButton = new Button{ - action = Action("Apply") { - container(getMutators(panels)) - } - } - - private val resetButton = new Button { - action = Action("Reset") { - panels = getPanels(container()) - } - } - - private val cancelButton = new Button{ - action = Action("Close") { - close - } - } - defaultButton = cancelButton - - private val botPanel = new BoxPanel(Orientation.Horizontal) { - border = new EmptyBorder(10, 0, 0, 0) - - contents += mutatorBox - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += addButton - - contents += Swing.HGlue - contents += Swing.RigidBox(new Dimension(30, 0)) - contents += applyButton - - contents += Swing.RigidBox(new Dimension(5, 0)) - contents += resetButton - - contents += Swing.RigidBox(new Dimension(5, 0)) - contents += cancelButton - } - - contents = new BorderPanel { - border = new EmptyBorder(5, 5, 5, 5) - - add(new ScrollPane(filterPanel), BorderPanel.Position.Center) - add(botPanel, BorderPanel.Position.South) - } - - private class Mutator_Panel(initials: Mutator_Markup) - extends BoxPanel(Orientation.Horizontal) - { - private val (_enabled, _color, _mutator) = initials - - private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs() - var focusList = List.empty[java.awt.Component] - private val enabledBox = new iCheckBox("Enabled", _enabled) - - border = new EmptyBorder(5, 5, 5, 5) - maximumSize = new Dimension(Integer.MAX_VALUE, 30) - background = _color - - contents += new Label(_mutator.name) { - preferredSize = new Dimension(175, 20) - horizontalAlignment = Alignment.Left - if (_mutator.description != "") tooltip = _mutator.description - } - contents += Swing.RigidBox(new Dimension(10, 0)) - contents += enabledBox - contents += Swing.RigidBox(new Dimension(5, 0)) - focusList = enabledBox.peer :: focusList - inputs.map( _ match { - case (n, c) => { - contents += Swing.RigidBox(new Dimension(10, 0)) - if (n != "") { - contents += new Label(n) - contents += Swing.RigidBox(new Dimension(5, 0)) - } - contents += c.asInstanceOf[Component] - - focusList = c.asInstanceOf[Component].peer :: focusList - } - case _ => - }) - - { - val t = this - contents += Swing.HGlue - contents += Swing.RigidBox(new Dimension(10, 0)) - - if (show_color_chooser) { - contents += new Button { - maximumSize = new Dimension(20, 20) - - action = Action("Color") { - t.background = - JColorChooser.showDialog(t.peer, "Choose new Color", t.background) - } - - focusList = this.peer :: focusList - } - contents += Swing.RigidBox(new Dimension(2, 0)) - } - - contents += new Button { - maximumSize = new Dimension(20, 20) - - action = Action("Up") { - movePanelUp(t) - } - - focusList = this.peer :: focusList - } - contents += Swing.RigidBox(new Dimension(2, 0)) - contents += new Button { - maximumSize = new Dimension(20, 20) - - action = Action("Down") { - movePanelDown(t) - } - - focusList = this.peer :: focusList - } - contents += Swing.RigidBox(new Dimension(2, 0)) - contents += new Button { - maximumSize = new Dimension(20, 20) - - action = Action("Del") { - removePanel(t) - } - - focusList = this.peer :: focusList - } - } - - focusList = focusList.reverse - - private def isRegex(regex: String): Boolean = { - try { - regex.r - - true - } catch { - case _: java.util.regex.PatternSyntaxException => false - } - } - - def get_Mutator_Markup: Mutator_Markup = { - def regexOrElse(regex: String, orElse: String): String = { - if (isRegex(regex)) regex - else orElse - } - - val m = _mutator match { - case Identity() => - Identity() - case Node_Expression(r, _, _, _) => - Node_Expression( - regexOrElse(inputs(2)._2.getString, r), - inputs(3)._2.getBool, - // "Parents" means "Show parents" or "Matching Children" - inputs(1)._2.getBool, - inputs(0)._2.getBool - ) - case Node_List(_, _, _, _) => - Node_List( - inputs(2)._2.getString.split(',').filter(_ != "").toList, - inputs(3)._2.getBool, - // "Parents" means "Show parents" or "Matching Children" - inputs(1)._2.getBool, - inputs(0)._2.getBool - ) - case Edge_Endpoints(_, _) => - Edge_Endpoints( - inputs(0)._2.getString, - inputs(1)._2.getString - ) - case Add_Node_Expression(r) => - Add_Node_Expression( - regexOrElse(inputs(0)._2.getString, r) - ) - case Add_Transitive_Closure(_, _) => - Add_Transitive_Closure( - inputs(0)._2.getBool, - inputs(1)._2.getBool - ) - case _ => - Identity() - } - - (enabledBox.selected, background, m) - } - - private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match { - case Node_Expression(regex, reverse, check_parents, check_children) => - List( - ("", new iCheckBox("Parents", check_children)), - ("", new iCheckBox("Children", check_parents)), - ("Regex", new iTextField(regex, x => !isRegex(x))), - ("", new iCheckBox(reverse_caption, reverse)) - ) - case Node_List(list, reverse, check_parents, check_children) => - List( - ("", new iCheckBox("Parents", check_children)), - ("", new iCheckBox("Children", check_parents)), - ("Names", new iTextField(list.mkString(","))), - ("", new iCheckBox(reverse_caption, reverse)) - ) - case Edge_Endpoints(source, dest) => - List( - ("Source", new iTextField(source)), - ("Destination", new iTextField(dest)) - ) - case Add_Node_Expression(regex) => - List( - ("Regex", new iTextField(regex, x => !isRegex(x))) - ) - case Add_Transitive_Closure(parents, children) => - List( - ("", new iCheckBox("Parents", parents)), - ("", new iCheckBox("Children", children)) - ) - case _ => Nil - } - } - - private trait Mutator_Input_Value - { - def getString: String - def getBool: Boolean - } - - private class iTextField(t: String, colorator: String => Boolean) - extends TextField(t) with Mutator_Input_Value - { - def this(t: String) = this(t, x => false) - - preferredSize = new Dimension(125, 18) - - reactions += { - case ValueChanged(_) => - if (colorator(text)) - background = Color.RED - else - background = Color.WHITE - } - - def getString = text - def getBool = true - } - - private class iCheckBox(t: String, s: Boolean) - extends CheckBox(t) with Mutator_Input_Value - { - selected = s - - def getString = "" - def getBool = selected - } - - private object focusTraversal - extends FocusTraversalPolicy - { - private var items = Vector[java.awt.Component]() - - def add(c: java.awt.Component) { - items = items :+ c - } - def addAll(cs: TraversableOnce[java.awt.Component]) { - items = items ++ cs - } - def clear() { - items = Vector[java.awt.Component]() - } - - def getComponentAfter(root: java.awt.Container, - c: java.awt.Component): java.awt.Component = { - val i = items.indexOf(c) - if (i < 0) { - getDefaultComponent(root) - } else { - items((i + 1) % items.length) - } - } - - def getComponentBefore(root: java.awt.Container, - c: java.awt.Component): java.awt.Component = { - val i = items.indexOf(c) - if (i < 0) { - getDefaultComponent(root) - } else { - items((i - 1) % items.length) - } - } - - def getFirstComponent(root: java.awt.Container): java.awt.Component = { - if (items.length > 0) - items(0) - else - null - } - - def getDefaultComponent(root: java.awt.Container) - : java.awt.Component = getFirstComponent(root) - - def getLastComponent(root: java.awt.Container): java.awt.Component = { - if (items.length > 0) - items.last - else - null - } - } -} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/mutator_event.scala --- a/src/Tools/Graphview/src/mutator_event.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -/* Title: Tools/Graphview/src/mutator_event.scala - Author: Markus Kaiser, TU Muenchen - -Events for dialog synchronization. -*/ - -package isabelle.graphview - - -import isabelle._ - -import scala.collection.mutable - -import java.awt.Color - - -object Mutator_Event -{ - type Mutator_Markup = (Boolean, Color, Mutator) - - sealed abstract class Message - case class Add(m: Mutator_Markup) extends Message - case class NewList(m: List[Mutator_Markup]) extends Message - - type Receiver = PartialFunction[Message, Unit] - - class Bus - { - private val receivers = new mutable.ListBuffer[Receiver] - - def += (r: Receiver) { GUI_Thread.require {}; receivers += r } - def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r } - def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) } - } -} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/popups.scala --- a/src/Tools/Graphview/src/popups.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -/* Title: Tools/Graphview/src/popups.scala - Author: Markus Kaiser, TU Muenchen - -PopupMenu generation for graph components. -*/ - -package isabelle.graphview - - -import isabelle._ -import isabelle.graphview.Mutators._ - -import javax.swing.JPopupMenu -import scala.swing.{Action, Menu, MenuItem, Separator} - - -object Popups -{ - def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]) - : JPopupMenu = - { - val visualizer = panel.visualizer - - val add_mutator = visualizer.model.Mutators.add _ - val curr = visualizer.model.current - - def filter_context(ls: List[String], reverse: Boolean, - caption: String, edges: Boolean) = - new Menu(caption) { - contents += new MenuItem(new Action("This") { - def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, false, false) - ) - ) - }) - - contents += new MenuItem(new Action("Family") { - def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, true, true) - ) - ) - }) - - contents += new MenuItem(new Action("Parents") { - def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, false, true) - ) - ) - }) - - contents += new MenuItem(new Action("Children") { - def apply = - add_mutator( - Mutators.create(visualizer, - Node_List(ls, reverse, true, false) - ) - ) - }) - - - if (edges) { - val outs = ls.map(l => (l, curr.imm_succs(l))) // FIXME iterator - .filter(_._2.size > 0).sortBy(_._1) - val ins = ls.map(l => (l, curr.imm_preds(l))) // FIXME iterator - .filter(_._2.size > 0).sortBy(_._1) - - if (outs.nonEmpty || ins.nonEmpty) { - contents += new Separator() - - contents += new Menu("Edge") { - if (outs.nonEmpty) { - contents += new MenuItem("From...") { - enabled = false - } - - outs.map( e => { - val (from, tos) = e - contents += new Menu(from) { - contents += new MenuItem("To..."){ - enabled = false - } - - tos.toList.sorted.distinct.map( to => { - contents += new MenuItem(new Action(to) { - def apply = - add_mutator( - Mutators.create(visualizer, Edge_Endpoints(from, to)) - ) - }) - }) - } - }) - } - if (outs.nonEmpty && ins.nonEmpty) { - contents += new Separator() - } - if (ins.nonEmpty) { - contents += new MenuItem("To...") { - enabled = false - } - - ins.map( e => { - val (to, froms) = e - contents += new Menu(to) { - contents += new MenuItem("From..."){ - enabled = false - } - - froms.toList.sorted.distinct.map( from => { - contents += new MenuItem(new Action(from) { - def apply = - add_mutator( - Mutators.create(visualizer, Edge_Endpoints(from, to)) - ) - }) - }) - } - }) - } - } - } - } - } - - val popup = new JPopupMenu() - - popup.add(new MenuItem(new Action("Remove all filters") { - def apply = visualizer.model.Mutators(Nil) - }).peer - ) - popup.add(new JPopupMenu.Separator) - - if (under_mouse.isDefined) { - val v = under_mouse.get - popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) { - enabled = false - }.peer) - - popup.add(filter_context(List(v), true, "Hide", true).peer) - popup.add(filter_context(List(v), false, "Show only", false).peer) - - popup.add(new JPopupMenu.Separator) - } - if (!selected.isEmpty) { - val text = { - if (selected.length > 1) { - "Multiple" - } else { - visualizer.Caption(selected.head) - } - } - - popup.add(new MenuItem("Selected: %s".format(text)) { - enabled = false - }.peer) - - popup.add(filter_context(selected, true, "Hide", true).peer) - popup.add(filter_context(selected, false, "Show only", false).peer) - popup.add(new JPopupMenu.Separator) - } - - - popup.add(new MenuItem(new Action("Fit to Window") { - def apply = panel.fit_to_window() - }).peer - ) - - popup - } -} diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/shapes.scala --- a/src/Tools/Graphview/src/shapes.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,255 +0,0 @@ -/* Title: Tools/Graphview/src/shapes.scala - Author: Markus Kaiser, TU Muenchen - -Drawable shapes. -*/ - -package isabelle.graphview - - -import java.awt.{BasicStroke, Graphics2D, Shape} -import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator} - - -object Shapes -{ - trait Node - { - def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape - def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit - } - - object Growing_Node extends Node - { - private val stroke = - new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) - - def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double = - { - val (x, y) = visualizer.Coordinates(peer.get) - val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g) - val w = bounds.getWidth + visualizer.pad_x - val h = bounds.getHeight + visualizer.pad_y - new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h) - } - - def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]) - { - val caption = visualizer.Caption(peer.get) - val bounds = g.getFontMetrics.getStringBounds(caption, g) - val s = shape(g, visualizer, peer) - - val (border, background, foreground) = visualizer.Color(peer) - g.setStroke(stroke) - g.setColor(border) - g.draw(s) - g.setColor(background) - g.fill(s) - g.setColor(foreground) - g.drawString(caption, - (s.getCenterX + (- bounds.getWidth / 2)).toFloat, - (s.getCenterY + 5).toFloat) - } - } - - object Dummy extends Node - { - private val stroke = - new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) - private val shape = new Rectangle2D.Double(-5, -5, 10, 10) - private val identity = new AffineTransform() - - def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape - - def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit = - paint_transformed(g, visualizer, peer, identity) - - def paint_transformed(g: Graphics2D, visualizer: Visualizer, - peer: Option[String], at: AffineTransform) - { - val (border, background, foreground) = visualizer.Color(peer) - g.setStroke(stroke) - g.setColor(border) - g.draw(at.createTransformedShape(shape)) - } - } - - trait Edge - { - def paint(g: Graphics2D, visualizer: Visualizer, - peer: (String, String), head: Boolean, dummies: Boolean) - } - - object Straight_Edge extends Edge - { - private val stroke = - new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) - - def paint(g: Graphics2D, visualizer: Visualizer, - peer: (String, String), head: Boolean, dummies: Boolean) - { - val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) - val ds = - { - val min = fy min ty - val max = fy max ty - visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max }) - } - val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) - - path.moveTo(fx, fy) - ds.foreach({case (x, y) => path.lineTo(x, y)}) - path.lineTo(tx, ty) - - if (dummies) { - ds.foreach({ - case (x, y) => { - val at = AffineTransform.getTranslateInstance(x, y) - Dummy.paint_transformed(g, visualizer, None, at) - } - }) - } - - g.setStroke(stroke) - g.setColor(visualizer.Color(peer)) - g.draw(path) - - if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) - } - } - - object Cardinal_Spline_Edge extends Edge - { - private val stroke = - new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) - private val slack = 0.1 - - def paint(g: Graphics2D, visualizer: Visualizer, - peer: (String, String), head: Boolean, dummies: Boolean) - { - val ((fx, fy), (tx, ty)) = - (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2)) - val ds = - { - val min = fy min ty - val max = fy max ty - visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max}) - } - - if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies) - else { - val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) - path.moveTo(fx, fy) - - val coords = ((fx, fy) :: ds ::: List((tx, ty))) - val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2) - - val (dx2, dy2) = - ((dx, dy) /: coords.sliding(3))({ - case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => { - val (dx2, dy2) = (rx - lx, ry - ly) - - path.curveTo(lx + slack * dx , ly + slack * dy, - mx - slack * dx2, my - slack * dy2, - mx , my) - (dx2, dy2) - } - }) - - val (lx, ly) = ds.last - path.curveTo(lx + slack * dx2, ly + slack * dy2, - tx - slack * dx2, ty - slack * dy2, - tx , ty) - - if (dummies) { - ds.foreach({ - case (x, y) => { - val at = AffineTransform.getTranslateInstance(x, y) - Dummy.paint_transformed(g, visualizer, None, at) - } - }) - } - - g.setStroke(stroke) - g.setColor(visualizer.Color(peer)) - g.draw(path) - - if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2))) - } - } - } - - object Arrow_Head - { - type Point = (Double, Double) - - private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = - { - def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = - { - val i = path.getPathIterator(null, 1.0) - val seg = Array[Double](0,0,0,0,0,0) - var p1 = (0.0, 0.0) - var p2 = (0.0, 0.0) - while (!i.isDone()) { - i.currentSegment(seg) match { - case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) - case PathIterator.SEG_LINETO => - p1 = p2 - p2 = (seg(0), seg(1)) - - if(shape.contains(seg(0), seg(1))) - return Some((p1, p2)) - case _ => - } - i.next() - } - None - } - - def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = - { - val ((fx, fy), (tx, ty)) = line - if (shape.contains(fx, fy) == shape.contains(tx, ty)) - None - else { - val (dx, dy) = (fx - tx, fy - ty) - if ((dx * dx + dy * dy) < 1.0) { - val at = AffineTransform.getTranslateInstance(fx, fy) - at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) - Some(at) - } - else { - val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) - if (shape.contains(fx, fy) == shape.contains(mx, my)) - binary_search(((mx, my), (tx, ty)), shape) - else - binary_search(((fx, fy), (mx, my)), shape) - } - } - } - - intersecting_line(path, shape) match { - case None => None - case Some(line) => binary_search(line, shape) - } - } - - def paint(g: Graphics2D, path: GeneralPath, shape: Shape) - { - position(path, shape) match { - case None => - case Some(at) => - val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) - arrow.moveTo(0, 0) - arrow.lineTo(-10, 4) - arrow.lineTo(-6, 0) - arrow.lineTo(-10, -4) - arrow.lineTo(0, 0) - arrow.transform(at) - - g.fill(arrow) - } - } - } -} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/src/visualizer.scala --- a/src/Tools/Graphview/src/visualizer.scala Tue Dec 30 11:50:34 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,215 +0,0 @@ -/* Title: Tools/Graphview/src/visualizer.scala - Author: Markus Kaiser, TU Muenchen - -Graph visualization parameters and interface state. -*/ - -package isabelle.graphview - - -import isabelle._ - -import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D} -import java.awt.image.BufferedImage -import javax.swing.JComponent - - -class Visualizer(val model: Model) -{ - visualizer => - - - /* font rendering information */ - - val font_family: String = "IsabelleText" - val font_size: Int = 14 - val font = new Font(font_family, Font.BOLD, font_size) - - val rendering_hints = - new RenderingHints( - RenderingHints.KEY_ANTIALIASING, - RenderingHints.VALUE_ANTIALIAS_ON) - - val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics - gfx.setFont(font) - gfx.setRenderingHints(rendering_hints) - - val font_metrics: FontMetrics = gfx.getFontMetrics(font) - - val tooltip_font_size: Int = 10 - - - /* rendering parameters */ - - val gap_x = 20 - val pad_x = 8 - val pad_y = 5 - - var arrow_heads = false - - object Colors - { - private val filter_colors = List( - new JColor(0xD9, 0xF2, 0xE2), // blue - new JColor(0xFF, 0xE7, 0xD8), // orange - new JColor(0xFF, 0xFF, 0xE5), // yellow - new JColor(0xDE, 0xCE, 0xFF), // lilac - new JColor(0xCC, 0xEB, 0xFF), // turquoise - new JColor(0xFF, 0xE5, 0xE5), // red - new JColor(0xE5, 0xE5, 0xD9) // green - ) - - private var curr : Int = -1 - def next(): JColor = - { - curr = (curr + 1) % filter_colors.length - filter_colors(curr) - } - } - - - object Coordinates - { - private var layout = Layout_Pendulum.empty_layout - - def apply(k: String): (Double, Double) = - layout.nodes.get(k) match { - case Some(c) => c - case None => (0, 0) - } - - def apply(e: (String, String)): List[(Double, Double)] = - layout.dummies.get(e) match { - case Some(ds) => ds - case None => Nil - } - - def reposition(k: String, to: (Double, Double)) - { - layout = layout.copy(nodes = layout.nodes + (k -> to)) - } - - def reposition(d: ((String, String), Int), to: (Double, Double)) - { - val (e, index) = d - layout.dummies.get(e) match { - case None => - case Some(ds) => - layout = layout.copy(dummies = - layout.dummies + (e -> - (ds.zipWithIndex :\ List.empty[(Double, Double)]) { - case ((t, i), n) => if (index == i) to :: n else t :: n - })) - } - } - - def translate(k: String, by: (Double, Double)) - { - val ((x, y), (dx, dy)) = (Coordinates(k), by) - reposition(k, (x + dx, y + dy)) - } - - def translate(d: ((String, String), Int), by: (Double, Double)) - { - val ((e, i),(dx, dy)) = (d, by) - val (x, y) = apply(e)(i) - reposition(d, (x + dx, y + dy)) - } - - def update_layout() - { - layout = - if (model.current.is_empty) Layout_Pendulum.empty_layout - else { - val max_width = - model.current.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) - } - } - - def bounds(): (Double, Double, Double, Double) = - model.visible_nodes_iterator.toList match { - case Nil => (0, 0, 0, 0) - case nodes => - val X: (String => Double) = (n => apply(n)._1) - val Y: (String => Double) = (n => apply(n)._2) - - (X(nodes.minBy(X)), Y(nodes.minBy(Y)), - X(nodes.maxBy(X)), Y(nodes.maxBy(Y))) - } - } - - object Drawer - { - def apply(g: Graphics2D, n: Option[String]) - { - n match { - case None => - case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n) - } - } - - def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) - { - Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies) - } - - def paint_all_visible(g: Graphics2D, dummies: Boolean) - { - g.setFont(font) - - g.setRenderingHints(rendering_hints) - - model.visible_edges_iterator.foreach(e => { - apply(g, e, arrow_heads, dummies) - }) - - model.visible_nodes_iterator.foreach(l => { - apply(g, Some(l)) - }) - } - - def shape(g: Graphics2D, n: Option[String]): Shape = - n match { - case None => Shapes.Dummy.shape(g, visualizer, None) - case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n) - } - } - - object Selection - { - private var selected: List[String] = Nil - - def apply() = selected - def apply(s: String) = selected.contains(s) - - def add(s: String) { selected = s :: selected } - def set(ss: List[String]) { selected = ss } - def clear() { selected = Nil } - } - - object Color - { - def apply(l: Option[String]): (JColor, JColor, JColor) = - l match { - case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK) - case Some(c) => { - if (Selection(c)) - (JColor.BLUE, JColor.GREEN, JColor.BLACK) - else - (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK) - } - } - - def apply(e: (String, String)): JColor = JColor.BLACK - } - - object Caption - { - def apply(key: String) = model.complete.get_node(key).name - } -} \ No newline at end of file diff -r 702e0971d617 -r 711c2446dc9d src/Tools/Graphview/visualizer.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Graphview/visualizer.scala Tue Dec 30 14:11:06 2014 +0100 @@ -0,0 +1,215 @@ +/* Title: Tools/Graphview/visualizer.scala + Author: Markus Kaiser, TU Muenchen + +Graph visualization parameters and interface state. +*/ + +package isabelle.graphview + + +import isabelle._ + +import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D} +import java.awt.image.BufferedImage +import javax.swing.JComponent + + +class Visualizer(val model: Model) +{ + visualizer => + + + /* font rendering information */ + + val font_family: String = "IsabelleText" + val font_size: Int = 14 + val font = new Font(font_family, Font.BOLD, font_size) + + val rendering_hints = + new RenderingHints( + RenderingHints.KEY_ANTIALIASING, + RenderingHints.VALUE_ANTIALIAS_ON) + + val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics + gfx.setFont(font) + gfx.setRenderingHints(rendering_hints) + + val font_metrics: FontMetrics = gfx.getFontMetrics(font) + + val tooltip_font_size: Int = 10 + + + /* rendering parameters */ + + val gap_x = 20 + val pad_x = 8 + val pad_y = 5 + + var arrow_heads = false + + object Colors + { + private val filter_colors = List( + new JColor(0xD9, 0xF2, 0xE2), // blue + new JColor(0xFF, 0xE7, 0xD8), // orange + new JColor(0xFF, 0xFF, 0xE5), // yellow + new JColor(0xDE, 0xCE, 0xFF), // lilac + new JColor(0xCC, 0xEB, 0xFF), // turquoise + new JColor(0xFF, 0xE5, 0xE5), // red + new JColor(0xE5, 0xE5, 0xD9) // green + ) + + private var curr : Int = -1 + def next(): JColor = + { + curr = (curr + 1) % filter_colors.length + filter_colors(curr) + } + } + + + object Coordinates + { + private var layout = Layout_Pendulum.empty_layout + + def apply(k: String): (Double, Double) = + layout.nodes.get(k) match { + case Some(c) => c + case None => (0, 0) + } + + def apply(e: (String, String)): List[(Double, Double)] = + layout.dummies.get(e) match { + case Some(ds) => ds + case None => Nil + } + + def reposition(k: String, to: (Double, Double)) + { + layout = layout.copy(nodes = layout.nodes + (k -> to)) + } + + def reposition(d: ((String, String), Int), to: (Double, Double)) + { + val (e, index) = d + layout.dummies.get(e) match { + case None => + case Some(ds) => + layout = layout.copy(dummies = + layout.dummies + (e -> + (ds.zipWithIndex :\ List.empty[(Double, Double)]) { + case ((t, i), n) => if (index == i) to :: n else t :: n + })) + } + } + + def translate(k: String, by: (Double, Double)) + { + val ((x, y), (dx, dy)) = (Coordinates(k), by) + reposition(k, (x + dx, y + dy)) + } + + def translate(d: ((String, String), Int), by: (Double, Double)) + { + val ((e, i),(dx, dy)) = (d, by) + val (x, y) = apply(e)(i) + reposition(d, (x + dx, y + dy)) + } + + def update_layout() + { + layout = + if (model.current.is_empty) Layout_Pendulum.empty_layout + else { + val max_width = + model.current.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) + } + } + + def bounds(): (Double, Double, Double, Double) = + model.visible_nodes_iterator.toList match { + case Nil => (0, 0, 0, 0) + case nodes => + val X: (String => Double) = (n => apply(n)._1) + val Y: (String => Double) = (n => apply(n)._2) + + (X(nodes.minBy(X)), Y(nodes.minBy(Y)), + X(nodes.maxBy(X)), Y(nodes.maxBy(Y))) + } + } + + object Drawer + { + def apply(g: Graphics2D, n: Option[String]) + { + n match { + case None => + case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n) + } + } + + def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) + { + Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies) + } + + def paint_all_visible(g: Graphics2D, dummies: Boolean) + { + g.setFont(font) + + g.setRenderingHints(rendering_hints) + + model.visible_edges_iterator.foreach(e => { + apply(g, e, arrow_heads, dummies) + }) + + model.visible_nodes_iterator.foreach(l => { + apply(g, Some(l)) + }) + } + + def shape(g: Graphics2D, n: Option[String]): Shape = + n match { + case None => Shapes.Dummy.shape(g, visualizer, None) + case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n) + } + } + + object Selection + { + private var selected: List[String] = Nil + + def apply() = selected + def apply(s: String) = selected.contains(s) + + def add(s: String) { selected = s :: selected } + def set(ss: List[String]) { selected = ss } + def clear() { selected = Nil } + } + + object Color + { + def apply(l: Option[String]): (JColor, JColor, JColor) = + l match { + case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK) + case Some(c) => { + if (Selection(c)) + (JColor.BLUE, JColor.GREEN, JColor.BLACK) + else + (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK) + } + } + + def apply(e: (String, String)): JColor = JColor.BLACK + } + + object Caption + { + def apply(key: String) = model.complete.get_node(key).name + } +} \ No newline at end of file