--- 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"
)
--- /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)
+ )
+ }
+ }
+ }
+}
--- /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))
+ }
+ }
+}
--- /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))
+ }
+ }
+}
--- /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() }
+}
--- /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
--- /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
--- /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
--- /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
+ }
+}
--- /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
--- 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)
- )
- }
- }
- }
-}
--- 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))
- }
- }
-}
--- 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))
- }
- }
-}
--- 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() }
-}
--- 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
--- 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
--- 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
--- 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
- }
-}
--- 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
--- 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
--- /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