# HG changeset patch # User wenzelm # Date 1420143781 -3600 # Node ID e067cd4f13d55485ff8b932fd5cfb74fcc7e8d9e # Parent 839f4d1a74679730ae522069bf342f07e812744c# Parent ef8104d6deb6f3debf19c730f0d5b03885bcc78d merged diff -r 839f4d1a7467 -r e067cd4f13d5 src/Pure/GUI/gui.scala --- 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 + "%;" } diff -r 839f4d1a7467 -r e067cd4f13d5 src/Pure/build-jars --- 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" diff -r 839f4d1a7467 -r e067cd4f13d5 src/Pure/library.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) diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/graph_panel.scala --- 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)) } } } diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/layout.scala --- /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)) + } + } +} diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/layout_pendulum.scala --- 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)) - } - } -} diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/main_panel.scala --- 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) diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/model.scala --- 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() } } diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/mutator.scala --- 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 +} diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/mutator_dialog.scala --- 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 diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/mutator_event.scala --- 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] diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/popups.scala --- 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 } diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/shapes.scala --- 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))) diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/Graphview/visualizer.scala --- 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 diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/jEdit/src/graphview_dockable.scala --- 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) diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/jEdit/src/pretty_text_area.scala --- 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 diff -r 839f4d1a7467 -r e067cd4f13d5 src/Tools/jEdit/src/token_markup.scala --- 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)