--- a/src/Pure/GUI/gui.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Pure/GUI/gui.scala Thu Jan 01 21:23:01 2015 +0100
@@ -215,20 +215,20 @@
/* font operations */
- def font_metrics(font: Font): LineMetrics =
+ def line_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
{
val font1 = new Font(family, font.getStyle, font.getSize)
- val size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight * font.getSize
+ val size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight * font.getSize
font1.deriveFont((scale * size).toInt)
}
def imitate_font_css(family: String, font: Font, scale: Double = 1.0): String =
{
val font1 = new Font(family, font.getStyle, font.getSize)
- val rel_size = font_metrics(font).getHeight.toDouble / font_metrics(font1).getHeight
+ val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
"font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
}
--- a/src/Pure/build-jars Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Pure/build-jars Thu Jan 01 21:23:01 2015 +0100
@@ -103,7 +103,7 @@
term.scala
term_xml.scala
"../Tools/Graphview/graph_panel.scala"
- "../Tools/Graphview/layout_pendulum.scala"
+ "../Tools/Graphview/layout.scala"
"../Tools/Graphview/main_panel.scala"
"../Tools/Graphview/model.scala"
"../Tools/Graphview/mutator_dialog.scala"
--- a/src/Pure/library.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Pure/library.scala Thu Jan 01 21:23:01 2015 +0100
@@ -9,6 +9,7 @@
import scala.collection.mutable
+import scala.util.matching.Regex
object Library
@@ -186,6 +187,12 @@
}
+ /* regular expressions */
+
+ def make_regex(s: String): Option[Regex] =
+ try { Some(new Regex(s)) } catch { case ERROR(_) => None }
+
+
/* canonical list operations */
def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
--- a/src/Tools/Graphview/graph_panel.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Thu Jan 01 21:23:01 2015 +0100
@@ -12,28 +12,24 @@
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
import java.awt.geom.{AffineTransform, Point2D}
import java.awt.image.BufferedImage
-import javax.swing.{JScrollPane, JComponent}
+import javax.swing.{JScrollPane, JComponent, SwingUtilities}
import scala.swing.{Panel, ScrollPane}
-import scala.swing.event._
+import scala.swing.event.{Event, Key, KeyTyped, MousePressed, MouseDragged,
+ MouseMoved, MouseClicked, MouseWheelMoved, MouseEvent}
-class Graph_Panel(
- val visualizer: Visualizer,
- make_tooltip: (JComponent, Int, Int, XML.Body) => String)
- extends ScrollPane
+class Graph_Panel(val visualizer: Visualizer) 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 {
+ visualizer.model.complete_graph.get_node(name).content match {
case Nil => null
- case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+ case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
}
case None => null
}
@@ -47,8 +43,11 @@
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
def node(at: Point2D): Option[String] =
+ {
+ val gfx = visualizer.graphics_context()
visualizer.model.visible_nodes_iterator
- .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
+ .find(name => visualizer.Drawer.shape(gfx, Some(name)).contains(at))
+ }
def refresh()
{
@@ -74,20 +73,27 @@
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
+ 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)
+ preferredSize =
+ new Dimension(
+ (math.abs(maxX - minX + px) * s).toInt,
+ (math.abs(maxY - minY + py) * s).toInt)
- revalidate()
- }
+ revalidate()
+ }
- override def paint(g: Graphics2D) {
+ override def paint(g: Graphics2D)
+ {
super.paintComponent(g)
+ g.setColor(visualizer.background_color)
+ g.fillRect(0, 0, peer.getWidth, peer.getHeight)
g.transform(Transform())
visualizer.Drawer.paint_all_visible(g, true)
@@ -102,14 +108,15 @@
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()
- }
+ 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() }
@@ -130,7 +137,8 @@
def scale_discrete: Double =
(_scale * visualizer.font_size).round.toDouble / visualizer.font_size
- def apply() = {
+ def apply() =
+ {
val (minX, minY, _, _) = visualizer.Coordinates.bounds()
val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
@@ -138,7 +146,8 @@
at
}
- def fit_to_window() {
+ def fit_to_window()
+ {
if (visualizer.model.visible_nodes_iterator.isEmpty)
rescale(1.0)
else {
@@ -150,7 +159,8 @@
}
}
- def pane_to_graph_coordinates(at: Point2D): Point2D = {
+ def pane_to_graph_coordinates(at: Point2D): Point2D =
+ {
val s = Transform.scale_discrete
val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
@@ -159,93 +169,97 @@
}
}
- object Interaction {
- object Keyboard {
- import scala.swing.event.Key._
-
- val react: PartialFunction[Event, Unit] = {
+ object Interaction
+ {
+ object Keyboard
+ {
+ 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()
+ def typed(c: Char, m: Key.Modifiers) =
+ c 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
+ object Mouse
+ {
type Dummy = ((String, String), Int)
private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
- val react: PartialFunction[Event, Unit] = {
+ 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 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)
+ 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({
+ {
+ val gfx = visualizer.graphics_context()
+ 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)
+ visualizer.Drawer.shape(gfx, None).contains(at.getX() - x, at.getY() - y)
}) match {
case None => None
case Some((name, (_, index))) => Some((name, index))
}
+ }
- def pressed(at: Point) {
+ 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
+ val d =
+ l match {
+ case Nil =>
+ dummy(c) match {
+ case Some(d) => List(d)
+ case None => Nil
+ }
+ case _ => Nil
}
-
- case _ => Nil
- }
-
draginfo = (at, l, d)
}
- def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) {
- import javax.swing.SwingUtilities
-
+ def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent)
+ {
val c = Transform.pane_to_graph_coordinates(at)
val p = node(c)
- def left_click() {
+ def left_click()
+ {
(p, m) match {
- case (Some(l), Control) => visualizer.Selection.add(l)
- case (None, Control) =>
+ case (Some(l), Key.Modifier.Control) => visualizer.Selection.add(l)
+ case (None, Key.Modifier.Control) =>
- case (Some(l), Shift) => visualizer.Selection.add(l)
- case (None, Shift) =>
+ case (Some(l), Key.Modifier.Shift) => visualizer.Selection.add(l)
+ case (None, Key.Modifier.Shift) =>
case (Some(l), _) => visualizer.Selection.set(List(l))
case (None, _) => visualizer.Selection.clear
}
}
- def right_click() {
+ def right_click()
+ {
val menu = Popups(panel, p, visualizer.Selection())
menu.show(panel.peer, at.x, at.y)
}
@@ -256,18 +270,18 @@
}
}
- def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) {
+ 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) => {
+ 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)))
@@ -277,7 +291,8 @@
}
}
- def wheel(rotation: Int, at: Point) {
+ 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))
@@ -287,11 +302,11 @@
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)
- )
+ 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.scala Thu Jan 01 21:23:01 2015 +0100
@@ -0,0 +1,278 @@
+/* Title: Tools/Graphview/layout.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Pendulum DAG layout algorithm.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+
+final case class Layout(
+ nodes: Layout.Coordinates,
+ dummies: Map[(Layout.Key, Layout.Key), List[Layout.Point]])
+
+object Layout
+{
+ 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])
+
+ val empty = Layout(Map.empty, Map.empty)
+
+ val pendulum_iterations = 10
+ val minimize_crossings_iterations = 40
+
+ def make(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout =
+ {
+ if (graph.is_empty) empty
+ 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/layout_pendulum.scala Thu Jan 01 11:12:15 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,275 +0,0 @@
-/* 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))
- }
- }
-}
--- a/src/Tools/Graphview/main_panel.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Thu Jan 01 21:23:01 2015 +0100
@@ -8,11 +8,8 @@
import isabelle._
-import isabelle.graphview.Mutators._
-import scala.collection.JavaConversions._
-import scala.swing.{BorderPanel, Button, BoxPanel,
- Orientation, Swing, CheckBox, Action, FileChooser}
+import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser}
import java.io.{File => JFile}
import java.awt.{Color, Dimension, Graphics2D}
@@ -23,16 +20,12 @@
import javax.swing.JComponent
-class Main_Panel(graph: Model.Graph) extends BorderPanel
+class Main_Panel(model: Model, visualizer: Visualizer) extends BorderPanel
{
focusable = true
requestFocus()
- val model = new Model(graph)
- val visualizer = new Visualizer(model)
-
- def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
- val graph_panel = new Graph_Panel(visualizer, make_tooltip)
+ val graph_panel = new Graph_Panel(visualizer)
listenTo(keys)
reactions += graph_panel.reactions
@@ -45,54 +38,44 @@
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 _ =>
+ val options_panel =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ new CheckBox() {
+ selected = visualizer.arrow_heads
+ action = Action("Arrow Heads") {
+ visualizer.arrow_heads = selected
+ graph_panel.repaint()
+ }
+ },
+ 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
- }
- }
- }
+ },
+ graph_panel.zoom,
+ new Button {
+ action = Action("Apply Layout") {
+ graph_panel.apply_layout()
+ }
+ },
+ new Button {
+ action = Action("Fit to Window") {
+ graph_panel.fit_to_window()
+ }
+ },
+ new Button {
+ action = Action("Colorations") {
+ color_dialog.open
+ }
+ },
+ new Button {
+ action = Action("Filters") {
+ mutator_dialog.open
+ }
+ })
add(graph_panel, BorderPanel.Position.Center)
add(options_panel, BorderPanel.Position.North)
--- a/src/Tools/Graphview/model.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/model.scala Thu Jan 01 21:23:01 2015 +0100
@@ -8,29 +8,27 @@
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))
- }
+class Mutator_Container(val available: List[Mutator])
+{
+ val events = new Mutator_Event.Bus
- def add(mutator: Mutator_Markup) = {
- _mutators = _mutators ::: List(mutator)
-
- events.event(Mutator_Event.Add(mutator))
- }
+ private var _mutators : List[Mutator.Info] = Nil
+ def apply() = _mutators
+ def apply(mutators: List[Mutator.Info])
+ {
+ _mutators = mutators
+ events.event(Mutator_Event.New_List(mutators))
+ }
+
+ def add(mutator: Mutator.Info)
+ {
+ _mutators = _mutators ::: List(mutator)
+ events.event(Mutator_Event.Add(mutator))
+ }
}
@@ -59,48 +57,45 @@
isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
}
-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
-
+class Model(val complete_graph: Model.Graph)
+{
+ val Mutators =
+ new Mutator_Container(
+ List(
+ Mutator.Node_Expression(".*", false, false, false),
+ Mutator.Node_List(Nil, false, false, false),
+ Mutator.Edge_Endpoints("", ""),
+ Mutator.Add_Node_Expression(""),
+ Mutator.Add_Transitive_Closure(true, true)))
+
+ val Colors =
+ new Mutator_Container(
+ List(
+ Mutator.Node_Expression(".*", false, false, false),
+ Mutator.Node_List(Nil, false, false, false)))
+
+ def visible_nodes_iterator: Iterator[String] = current_graph.keys_iterator
+
def visible_edges_iterator: Iterator[(String, String)] =
- current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
-
- def complete = graph
- def current: Model.Graph =
- (graph /: Mutators()) {
- case (g, (enabled, _, mutator)) => {
- if (!enabled) g
- else mutator.mutate(graph, g)
- }
- }
-
+ current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))
+
+ def current_graph: Model.Graph =
+ (complete_graph /: Mutators()) {
+ case (g, m) => if (!m.enabled) g else m.mutator.mutate(complete_graph, g)
+ }
+
private var _colors = Map.empty[String, Color]
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)
- })
- }
- })
+
+ private def build_colors()
+ {
+ _colors =
+ (Map.empty[String, Color] /: Colors()) {
+ case (colors, m) =>
+ (colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
+ case (colors, k) => colors + (k -> m.color)
+ }
+ }
}
Colors.events += { case _ => build_colors() }
}
--- a/src/Tools/Graphview/mutator.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala Thu Jan 01 21:23:01 2015 +0100
@@ -13,135 +13,109 @@
import scala.collection.immutable.SortedSet
-trait Mutator
+object Mutator
{
- val name: String
- val description: String
- def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
+ sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator)
- override def toString: String = name
-}
-
-trait Filter extends Mutator
-{
- def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
- def filter(sub: Model.Graph) : Model.Graph
-}
+ def make(visualizer: Visualizer, m: Mutator): Info =
+ Info(true, visualizer.Colors.next, m)
-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
+ 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)
+ def filter(graph: Model.Graph) : Model.Graph = pred(graph)
}
- class Graph_Mutator(val name: String, val description: String,
- pred: (Model.Graph, Model.Graph) => Model.Graph)
- extends Mutator
+ 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)
+ def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph =
+ pred(complete_graph, graph)
}
- class Node_Filter(name: String, description: String,
+ 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 (
+ extends Graph_Filter(name, description, g => g.restrict(pred(g, _)))
- 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 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)
+ 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, _)))))
- 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(
+ "Identity",
+ "Does not change the graph.",
+ g => g)
- "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_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)
+ 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)
- )
+ "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)
- )
+ "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]) = {
-
+ 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))
- }
-
+ val with_nodes =
+ (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key)))
+
// Add Edges
(with_nodes /: keys) {
(gv, key) => {
@@ -156,44 +130,47 @@
}
}
-
add_edges(
add_edges(gv, from.imm_preds(key), false),
- from.imm_succs(key), true
- )
+ 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_graph, graph) =>
+ add_node_group(complete_graph, graph,
+ complete_graph.keys.filter(k => (regex.r findFirstIn k).isDefined).toList))
- "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_graph, graph) => {
+ val withparents =
+ if (parents) add_node_group(complete_graph, graph, complete_graph.all_preds(graph.keys))
+ else graph
+ if (children)
+ add_node_group(complete_graph, withparents, complete_graph.all_succs(graph.keys))
+ else withparents
+ })
+}
- "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
+trait Mutator
+{
+ val name: String
+ val description: String
+ def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph
+
+ override def toString: String = name
+}
+
+trait Filter extends Mutator
+{
+ def mutate(complete_graph: Model.Graph, graph: Model.Graph) = filter(graph)
+ def filter(graph: Model.Graph) : Model.Graph
+}
--- a/src/Tools/Graphview/mutator_dialog.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Thu Jan 01 21:23:01 2015 +0100
@@ -13,9 +13,8 @@
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.{Dialog, Button, BoxPanel, Swing, Orientation, ComboBox, Action,
+ Dimension, BorderPanel, ScrollPane, Label, CheckBox, Alignment, Component, TextField}
import scala.swing.event.ValueChanged
@@ -27,173 +26,168 @@
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]) {
+ private def panels_=(panels: List[Mutator_Panel])
+ {
_panels = panels
- paintPanels
+ paint_panels()
}
- container.events += {
- case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
- case Mutator_Event.NewList(ms) => panels = getPanels(ms)
+ container.events +=
+ {
+ case Mutator_Event.Add(m) => add_panel(new Mutator_Panel(m))
+ case Mutator_Event.New_List(ms) => panels = get_panels(ms)
}
- override def open() {
- if (!visible)
- panels = getPanels(container())
-
+ override def open()
+ {
+ if (!visible) panels = get_panels(container())
super.open
}
minimumSize = new Dimension(700, 200)
preferredSize = new Dimension(1000, 300)
- peer.setFocusTraversalPolicy(focusTraversal)
+ peer.setFocusTraversalPolicy(Focus_Traveral_Policy)
- private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] =
- m.filter(_ match {case (_, _, Identity()) => false; case _ => true})
+ private def get_panels(m: List[Mutator.Info]): List[Mutator_Panel] =
+ m.filter({ case Mutator.Info(_, _, Mutator.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 get_mutators(panels: List[Mutator_Panel]): List[Mutator.Info] =
+ panels.map(panel => panel.get_mutator)
- 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
- }
+ 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
- }
+ 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) = {
+ private def removePanel(m: Mutator_Panel)
+ {
panels = panels.filter(_ != m).toList
}
- private def addPanel(m: Mutator_Panel) = {
+ private def add_panel(m: Mutator_Panel)
+ {
panels = panels ::: List(m)
}
- def paintPanels = {
- focusTraversal.clear
- filterPanel.contents.clear
+ def paint_panels()
+ {
+ Focus_Traveral_Policy.clear
+ filter_panel.contents.clear
panels.map(x => {
- filterPanel.contents += x
- focusTraversal.addAll(x.focusList)
+ filter_panel.contents += x
+ Focus_Traveral_Policy.addAll(x.focusList)
})
- filterPanel.contents += Swing.VGlue
+ filter_panel.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
+ Focus_Traveral_Policy.add(mutator_box.peer.asInstanceOf[java.awt.Component])
+ Focus_Traveral_Policy.add(add_button.peer)
+ Focus_Traveral_Policy.add(apply_button.peer)
+ Focus_Traveral_Policy.add(cancel_button.peer)
+ filter_panel.revalidate
+ filter_panel.repaint
}
- val filterPanel = new BoxPanel(Orientation.Vertical) {}
+ val filter_panel = new BoxPanel(Orientation.Vertical) {}
- private val mutatorBox = new ComboBox[Mutator](container.available)
+ private val mutator_box = new ComboBox[Mutator](container.available)
- private val addButton: Button = new Button{
+ private val add_button = new Button {
action = Action("Add") {
- addPanel(
- new Mutator_Panel((true, visualizer.Colors.next,
- mutatorBox.selection.item))
- )
+ add_panel(
+ new Mutator_Panel(Mutator.Info(true, visualizer.Colors.next, mutator_box.selection.item)))
}
}
- private val applyButton = new Button{
- action = Action("Apply") {
- container(getMutators(panels))
- }
+ private val apply_button = new Button {
+ action = Action("Apply") { container(get_mutators(panels)) }
}
- private val resetButton = new Button {
- action = Action("Reset") {
- panels = getPanels(container())
- }
+ private val reset_button = new Button {
+ action = Action("Reset") { panels = get_panels(container()) }
}
- private val cancelButton = new Button{
- action = Action("Close") {
- close
- }
- }
- defaultButton = cancelButton
+ private val cancel_button = new Button {
+ action = Action("Close") { close }
+ }
+ defaultButton = cancel_button
private val botPanel = new BoxPanel(Orientation.Horizontal) {
border = new EmptyBorder(10, 0, 0, 0)
- contents += mutatorBox
+ contents += mutator_box
contents += Swing.RigidBox(new Dimension(10, 0))
- contents += addButton
+ contents += add_button
contents += Swing.HGlue
contents += Swing.RigidBox(new Dimension(30, 0))
- contents += applyButton
+ contents += apply_button
contents += Swing.RigidBox(new Dimension(5, 0))
- contents += resetButton
+ contents += reset_button
contents += Swing.RigidBox(new Dimension(5, 0))
- contents += cancelButton
+ contents += cancel_button
}
-
+
contents = new BorderPanel {
border = new EmptyBorder(5, 5, 5, 5)
- add(new ScrollPane(filterPanel), BorderPanel.Position.Center)
+ add(new ScrollPane(filter_panel), BorderPanel.Position.Center)
add(botPanel, BorderPanel.Position.South)
}
- private class Mutator_Panel(initials: Mutator_Markup)
+ private class Mutator_Panel(initials: Mutator.Info)
extends BoxPanel(Orientation.Horizontal)
{
- private val (_enabled, _color, _mutator) = initials
-
- private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
+ private val inputs: List[(String, Input)] = get_inputs()
var focusList = List.empty[java.awt.Component]
- private val enabledBox = new iCheckBox("Enabled", _enabled)
+ private val enabledBox = new Check_Box_Input("Enabled", initials.enabled)
border = new EmptyBorder(5, 5, 5, 5)
maximumSize = new Dimension(Integer.MAX_VALUE, 30)
- background = _color
+ background = initials.color
- contents += new Label(_mutator.name) {
+ contents += new Label(initials.mutator.name) {
preferredSize = new Dimension(175, 20)
horizontalAlignment = Alignment.Left
- if (_mutator.description != "") tooltip = _mutator.description
+ if (initials.mutator.description != "") tooltip = initials.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))
+ 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 _ =>
})
@@ -249,179 +243,132 @@
focusList = focusList.reverse
- private def isRegex(regex: String): Boolean = {
- try {
- regex.r
+ def get_mutator: Mutator.Info =
+ {
+ val m =
+ initials.mutator match {
+ case Mutator.Identity() =>
+ Mutator.Identity()
+ case Mutator.Node_Expression(r, _, _, _) =>
+ val r1 = inputs(2)._2.string
+ Mutator.Node_Expression(
+ if (Library.make_regex(r1).isDefined) r1 else r,
+ inputs(3)._2.bool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.bool,
+ inputs(0)._2.bool)
+ case Mutator.Node_List(_, _, _, _) =>
+ Mutator.Node_List(
+ inputs(2)._2.string.split(',').filter(_ != "").toList,
+ inputs(3)._2.bool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.bool,
+ inputs(0)._2.bool)
+ case Mutator.Edge_Endpoints(_, _) =>
+ Mutator.Edge_Endpoints(
+ inputs(0)._2.string,
+ inputs(1)._2.string)
+ case Mutator.Add_Node_Expression(r) =>
+ val r1 = inputs(0)._2.string
+ Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
+ case Mutator.Add_Transitive_Closure(_, _) =>
+ Mutator.Add_Transitive_Closure(
+ inputs(0)._2.bool,
+ inputs(1)._2.bool)
+ case _ =>
+ Mutator.Identity()
+ }
- true
- } catch {
- case _: java.util.regex.PatternSyntaxException => false
- }
+ Mutator.Info(enabledBox.selected, background, m)
}
-
- def get_Mutator_Markup: Mutator_Markup = {
- def regexOrElse(regex: String, orElse: String): String = {
- if (isRegex(regex)) regex
- else orElse
+
+ private def get_inputs(): List[(String, Input)] =
+ initials.mutator match {
+ case Mutator.Node_Expression(regex, reverse, check_parents, check_children) =>
+ List(
+ ("", new Check_Box_Input("Parents", check_children)),
+ ("", new Check_Box_Input("Children", check_parents)),
+ ("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)),
+ ("", new Check_Box_Input(reverse_caption, reverse)))
+ case Mutator.Node_List(list, reverse, check_parents, check_children) =>
+ List(
+ ("", new Check_Box_Input("Parents", check_children)),
+ ("", new Check_Box_Input("Children", check_parents)),
+ ("Names", new Text_Field_Input(list.mkString(","))),
+ ("", new Check_Box_Input(reverse_caption, reverse)))
+ case Mutator.Edge_Endpoints(source, dest) =>
+ List(
+ ("Source", new Text_Field_Input(source)),
+ ("Destination", new Text_Field_Input(dest)))
+ case Mutator.Add_Node_Expression(regex) =>
+ List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)))
+ case Mutator.Add_Transitive_Closure(parents, children) =>
+ List(
+ ("", new Check_Box_Input("Parents", parents)),
+ ("", new Check_Box_Input("Children", children)))
+ case _ => Nil
}
-
- 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
+ private trait Input
{
- def getString: String
- def getBool: Boolean
+ def string: String
+ def bool: Boolean
}
- private class iTextField(t: String, colorator: String => Boolean)
- extends TextField(t) with Mutator_Input_Value
+ private class Text_Field_Input(txt: String, check: String => Boolean = (_: String) => true)
+ extends TextField(txt) with Input
{
- def this(t: String) = this(t, x => false)
-
preferredSize = new Dimension(125, 18)
- reactions += {
+ private val default_foreground = foreground
+ reactions +=
+ {
case ValueChanged(_) =>
- if (colorator(text))
- background = Color.RED
- else
- background = Color.WHITE
+ foreground = if (check(text)) default_foreground else visualizer.error_color
}
- def getString = text
- def getBool = true
+ def string = text
+ def bool = true
}
- private class iCheckBox(t: String, s: Boolean)
- extends CheckBox(t) with Mutator_Input_Value
+ private class Check_Box_Input(txt: String, s: Boolean) extends CheckBox(txt) with Input
{
selected = s
- def getString = ""
- def getBool = selected
+ def string = ""
+ def bool = selected
}
- private object focusTraversal
- extends FocusTraversalPolicy
+ private object Focus_Traveral_Policy extends FocusTraversalPolicy
{
- private var items = Vector[java.awt.Component]()
+ private var items = Vector.empty[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 add(c: java.awt.Component) { items = items :+ c }
+ def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs }
+ def clear() { items = Vector.empty }
- def getComponentAfter(root: java.awt.Container,
- c: java.awt.Component): 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)
- }
+ if (i < 0) getDefaultComponent(root)
+ else items((i + 1) % items.length)
}
- def getComponentBefore(root: java.awt.Container,
- c: java.awt.Component): java.awt.Component = {
+ 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)
- }
+ 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 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 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
- }
+ 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/mutator_event.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/mutator_event.scala Thu Jan 01 21:23:01 2015 +0100
@@ -16,11 +16,9 @@
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
+ case class Add(m: Mutator.Info) extends Message
+ case class New_List(m: List[Mutator.Info]) extends Message
type Receiver = PartialFunction[Message, Unit]
--- a/src/Tools/Graphview/popups.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/popups.scala Thu Jan 01 21:23:01 2015 +0100
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.graphview.Mutators._
import javax.swing.JPopupMenu
import scala.swing.{Action, Menu, MenuItem, Separator}
@@ -16,131 +15,113 @@
object Popups
{
- def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
- : JPopupMenu =
+ 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
+ val curr = visualizer.model.current_graph
- def filter_context(ls: List[String], reverse: Boolean,
- caption: String, edges: Boolean) =
+ def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) =
new Menu(caption) {
- contents += new MenuItem(new Action("This") {
+ contents +=
+ new MenuItem(new Action("This") {
def apply =
- add_mutator(
- Mutators.create(visualizer,
- Node_List(ls, reverse, false, false)
- )
- )
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, false)))
})
- contents += new MenuItem(new Action("Family") {
+ contents +=
+ new MenuItem(new Action("Family") {
def apply =
- add_mutator(
- Mutators.create(visualizer,
- Node_List(ls, reverse, true, true)
- )
- )
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, true)))
})
- contents += new MenuItem(new Action("Parents") {
+ contents +=
+ new MenuItem(new Action("Parents") {
def apply =
- add_mutator(
- Mutators.create(visualizer,
- Node_List(ls, reverse, false, true)
- )
- )
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, true)))
})
- contents += new MenuItem(new Action("Children") {
+ contents +=
+ new MenuItem(new Action("Children") {
def apply =
- add_mutator(
- Mutators.create(visualizer,
- Node_List(ls, reverse, true, false)
- )
- )
+ add_mutator(Mutator.make(visualizer, Mutator.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)
+ 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
- }
+ 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 }
- 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(
+ Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
+ })
+ })
+ }
+ })
+ }
+ if (outs.nonEmpty && ins.nonEmpty) { contents += new Separator() }
+ if (ins.nonEmpty) {
+ 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))
- )
- })
- })
- }
- })
+ 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(
+ Mutator.make(visualizer, Mutator.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") {
+ popup.add(
+ new MenuItem(
+ new Action("Remove all filters") {
def apply = visualizer.model.Mutators(Nil)
- }).peer
- )
+ }).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(
+ 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)
@@ -148,28 +129,19 @@
popup.add(new JPopupMenu.Separator)
}
if (!selected.isEmpty) {
- val text = {
- if (selected.length > 1) {
- "Multiple"
- } else {
- visualizer.Caption(selected.head)
- }
- }
+ 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(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.add(
+ new MenuItem(new Action("Fit to Window") { def apply = panel.fit_to_window() }).peer)
popup
}
--- a/src/Tools/Graphview/shapes.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Thu Jan 01 21:23:01 2015 +0100
@@ -28,8 +28,9 @@
{
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
+ val m = visualizer.metrics()
+ val w = bounds.getWidth + m.pad_x
+ val h = bounds.getHeight + m.pad_y
new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
}
@@ -39,13 +40,13 @@
val bounds = g.getFontMetrics.getStringBounds(caption, g)
val s = shape(g, visualizer, peer)
- val (border, background, foreground) = visualizer.Color(peer)
+ val c = visualizer.node_color(peer)
g.setStroke(stroke)
- g.setColor(border)
+ g.setColor(c.border)
g.draw(s)
- g.setColor(background)
+ g.setColor(c.background)
g.fill(s)
- g.setColor(foreground)
+ g.setColor(c.foreground)
g.drawString(caption,
(s.getCenterX + (- bounds.getWidth / 2)).toFloat,
(s.getCenterY + 5).toFloat)
@@ -67,9 +68,9 @@
def paint_transformed(g: Graphics2D, visualizer: Visualizer,
peer: Option[String], at: AffineTransform)
{
- val (border, background, foreground) = visualizer.Color(peer)
+ val c = visualizer.node_color(peer)
g.setStroke(stroke)
- g.setColor(border)
+ g.setColor(c.border)
g.draw(at.createTransformedShape(shape))
}
}
@@ -111,7 +112,7 @@
}
g.setStroke(stroke)
- g.setColor(visualizer.Color(peer))
+ g.setColor(visualizer.edge_color(peer))
g.draw(path)
if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
@@ -171,7 +172,7 @@
}
g.setStroke(stroke)
- g.setColor(visualizer.Color(peer))
+ g.setColor(visualizer.edge_color(peer))
g.draw(path)
if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
--- a/src/Tools/Graphview/visualizer.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Thu Jan 01 21:23:01 2015 +0100
@@ -9,7 +9,8 @@
import isabelle._
-import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
+import java.awt.{Font, FontMetrics, Color, Shape, RenderingHints, Graphics2D}
+import java.awt.font.FontRenderContext
import java.awt.image.BufferedImage
import javax.swing.JComponent
@@ -19,48 +20,73 @@
visualizer =>
+ /* tooltips */
+
+ def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
+
+
+ /* main colors */
+
+ def foreground_color: Color = Color.BLACK
+ def foreground1_color: Color = Color.GRAY
+ def background_color: Color = Color.WHITE
+ def selection_color: Color = Color.GREEN
+ def error_color: Color = Color.RED
+
+
/* font rendering information */
- val font_family: String = "IsabelleText"
- val font_size: Int = 14
- val font = new Font(font_family, Font.BOLD, font_size)
+ def font_size: Int = 14
+ def font(): Font = new Font("IsabelleText", 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_render_context = new FontRenderContext(null, true, false)
+
+ def graphics_context(): Graphics2D =
+ {
+ val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics
+ gfx.setFont(font())
+ gfx.setRenderingHints(rendering_hints)
+ gfx
+ }
- val font_metrics: FontMetrics = gfx.getFontMetrics(font)
+ class Metrics private[Visualizer]
+ {
+ private val f = font()
+ def string_bounds(s: String) = f.getStringBounds(s, font_render_context)
+ private val specimen = string_bounds("mix")
- val tooltip_font_size: Int = 10
+ def char_width: Double = specimen.getWidth / 3
+ def line_height: Double = specimen.getHeight
+ def gap_x: Double = char_width * 2.5
+ def pad_x: Double = char_width * 0.5
+ def pad_y: Double = line_height * 0.25
+ }
+ def metrics(): Metrics = new Metrics
/* 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
+ new Color(0xD9, 0xF2, 0xE2), // blue
+ new Color(0xFF, 0xE7, 0xD8), // orange
+ new Color(0xFF, 0xFF, 0xE5), // yellow
+ new Color(0xDE, 0xCE, 0xFF), // lilac
+ new Color(0xCC, 0xEB, 0xFF), // turquoise
+ new Color(0xFF, 0xE5, 0xE5), // red
+ new Color(0xE5, 0xE5, 0xD9) // green
)
private var curr : Int = -1
- def next(): JColor =
+ def next(): Color =
{
curr = (curr + 1) % filter_colors.length
filter_colors(curr)
@@ -70,7 +96,7 @@
object Coordinates
{
- private var layout = Layout_Pendulum.empty_layout
+ private var layout = Layout.empty
def apply(k: String): (Double, Double) =
layout.nodes.get(k) match {
@@ -119,15 +145,17 @@
def update_layout()
{
layout =
- if (model.current.is_empty) Layout_Pendulum.empty_layout
+ if (model.current_graph.is_empty) Layout.empty
else {
+ val m = metrics()
+
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)
+ model.current_graph.iterator.map({ case (_, (info, _)) =>
+ m.string_bounds(info.name).getWidth }).max
+ val box_distance = max_width + m.pad_x + m.gap_x
+ def box_height(n: Int): Double = (m.line_height + m.pad_y) * (5 max n)
+
+ Layout.make(model.current_graph, box_distance, box_height _)
}
}
@@ -192,24 +220,22 @@
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)
- }
- }
+ sealed case class Node_Color(border: Color, background: Color, foreground: Color)
- def apply(e: (String, String)): JColor = JColor.BLACK
- }
+ def node_color(l: Option[String]): Node_Color =
+ l match {
+ case None =>
+ Node_Color(foreground1_color, background_color, foreground_color)
+ case Some(c) if Selection(c) =>
+ Node_Color(foreground_color, selection_color, foreground_color)
+ case Some(c) =>
+ Node_Color(foreground_color, model.colors.getOrElse(c, background_color), foreground_color)
+ }
+
+ def edge_color(e: (String, String)): Color = foreground_color
object Caption
{
- def apply(key: String) = model.complete.get_node(key).name
+ def apply(key: String) = model.complete_graph.get_node(key).name
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Thu Jan 01 21:23:01 2015 +0100
@@ -49,18 +49,20 @@
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val snapshot = Graphview_Dockable.implicit_snapshot
- private val graph = Graphview_Dockable.implicit_graph
+ private val graph_result = Graphview_Dockable.implicit_graph
private val window_focus_listener =
new WindowFocusListener {
- def windowGainedFocus(e: WindowEvent) { Graphview_Dockable.set_implicit(snapshot, graph) }
+ def windowGainedFocus(e: WindowEvent) {
+ Graphview_Dockable.set_implicit(snapshot, graph_result) }
def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
}
val graphview =
- graph match {
- case Exn.Res(proper_graph) =>
- new isabelle.graphview.Main_Panel(proper_graph) {
+ graph_result match {
+ case Exn.Res(graph) =>
+ val model = new isabelle.graphview.Model(graph)
+ val visualizer = new isabelle.graphview.Visualizer(model) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
Pretty_Tooltip.invoke(() =>
@@ -71,7 +73,14 @@
})
null
}
+ override def foreground_color = view.getTextArea.getPainter.getForeground
+ override def background_color = view.getTextArea.getPainter.getBackground
+ override def selection_color = view.getTextArea.getPainter.getSelectionColor
+ override def error_color = PIDE.options.color_value("error_color")
+ override def font_size = view.getTextArea.getPainter.getFont.getSize
+ override def font = view.getTextArea.getPainter.getFont
}
+ new isabelle.graphview.Main_Panel(model, visualizer)
case Exn.Exn(exn) => new TextArea(Exn.message(exn))
}
set_content(graphview)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Jan 01 21:23:01 2015 +0100
@@ -212,8 +212,8 @@
text_field.getText match {
case null | "" => (None, true)
case s =>
- try { (Some(new Regex(s)), true) }
- catch { case ERROR(_) => (None, false) }
+ val re = Library.make_regex(s)
+ (re, re.isDefined)
}
if (current_search_pattern != pattern) {
current_search_pattern = pattern
--- a/src/Tools/jEdit/src/token_markup.scala Thu Jan 01 11:12:15 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Thu Jan 01 21:23:01 2015 +0100
@@ -90,8 +90,8 @@
def shift(y: Float): Font =
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
- val m0 = GUI.font_metrics(font0)
- val m1 = GUI.font_metrics(font1)
+ val m0 = GUI.line_metrics(font0)
+ val m1 = GUI.line_metrics(font1)
val a = m1.getAscent - m0.getAscent
val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
if (a > 0.0f) shift(a)