more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
misc tuning;
tuned signature;
--- a/src/Pure/General/graph.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Pure/General/graph.scala Sat Jan 03 20:22:27 2015 +0100
@@ -21,15 +21,13 @@
def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
new Graph[Key, A](SortedMap.empty(ord))
- def make[Key, A](entries: List[((Key, A), List[Key])], converse: Boolean = false)(
+ def make[Key, A](entries: List[((Key, A), List[Key])])(
implicit ord: Ordering[Key]): Graph[Key, A] =
{
val graph1 =
(empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
val graph2 =
- (graph1 /: entries) { case (graph, ((x, _), ys)) =>
- if (converse) (graph /: ys)(_.add_edge(_, x)) else (graph /: ys)(_.add_edge(x, _))
- }
+ (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
graph2
}
@@ -46,11 +44,11 @@
list(pair(pair(key, info), list(key)))(graph.dest)
})
- def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A], converse: Boolean = false)(
+ def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
((body: XML.Body) => {
import XML.Decode._
- make(list(pair(pair(key, info), list(key)))(body), converse)(ord)
+ make(list(pair(pair(key, info), list(key)))(body))(ord)
})
}
--- a/src/Pure/General/graph_display.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Pure/General/graph_display.scala Sat Jan 03 20:22:27 2015 +0100
@@ -13,56 +13,52 @@
type Entry = ((String, (String, XML.Body)), List[String])
- /* node names */
+ /* graph structure */
- object Name
+ object Node
{
- val dummy: Name = Name("", "")
+ val dummy: Node = Node("", "")
- object Ordering extends scala.math.Ordering[Name]
+ object Ordering extends scala.math.Ordering[Node]
{
- def compare(name1: Name, name2: Name): Int =
- name1.name compare name2.name match {
- case 0 => name1.ident compare name2.ident
+ def compare(node1: Node, node2: Node): Int =
+ node1.name compare node2.name match {
+ case 0 => node1.ident compare node2.ident
case ord => ord
}
}
}
-
- sealed case class Name(name: String, ident: String)
+ sealed case class Node(name: String, ident: String)
{
+ def is_dummy: Boolean = this == Node.dummy
override def toString: String = name
}
-
- /* graph structure */
+ type Edge = (Node, Node)
- type Graph = isabelle.Graph[Name, XML.Body]
+ type Graph = isabelle.Graph[Node, XML.Body]
- val empty_graph: Graph = isabelle.Graph.empty(Name.Ordering)
+ val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering)
def build_graph(entries: List[Entry]): Graph =
{
- val the_key =
- (Map.empty[String, Name] /: entries) {
- case (m, ((ident, (name, _)), _)) => m + (ident -> Name(name, ident))
+ val node =
+ (Map.empty[String, Node] /: entries) {
+ case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
}
(((empty_graph /: entries) {
- case (g, ((ident, (_, content)), _)) => g.new_node(the_key(ident), content)
+ case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
}) /: entries) {
case (g1, ((ident, _), parents)) =>
- (g1 /: parents) { case (g2, parent) => g2.add_edge(the_key(parent), the_key(ident)) }
+ (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
}
}
def decode_graph(body: XML.Body): Graph =
- {
- val entries =
- {
- import XML.Decode._
- list(pair(pair(string, pair(string, x => x)), list(string)))(body)
- }
- build_graph(entries)
- }
+ build_graph(
+ {
+ import XML.Decode._
+ list(pair(pair(string, pair(string, x => x)), list(string)))(body)
+ })
}
--- a/src/Tools/Graphview/graph_panel.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sat Jan 03 20:22:27 2015 +0100
@@ -27,9 +27,9 @@
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_graph.get_node(name).content match {
+ find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+ case Some(node) =>
+ visualizer.model.complete_graph.get_node(node) match {
case Nil => null
case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
}
@@ -45,11 +45,11 @@
peer.getVerticalScrollBar.setUnitIncrement(10)
- def node(at: Point2D): Option[String] =
+ def find_node(at: Point2D): Option[Graph_Display.Node] =
{
val m = visualizer.metrics()
visualizer.model.visible_nodes_iterator
- .find(name => visualizer.Drawer.shape(m, Some(name)).contains(at))
+ .find(node => visualizer.Drawer.shape(m, node).contains(at))
}
def refresh()
@@ -181,9 +181,9 @@
object Mouse
{
- type Dummy = ((String, String), Int)
+ type Dummy = (Graph_Display.Edge, Int)
- private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
+ private var draginfo: (Point, List[Graph_Display.Node], List[Dummy]) = null
val react: PartialFunction[Event, Unit] =
{
@@ -199,23 +199,27 @@
{
val m = visualizer.metrics()
visualizer.model.visible_edges_iterator.map(
- i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({
- case (_, ((x, y), _)) =>
- visualizer.Drawer.shape(m, None).contains(at.getX() - x, at.getY() - y)
- }) match {
- case None => None
- case Some((name, (_, index))) => Some((name, index))
- }
+ edge => visualizer.Coordinates(edge).zipWithIndex.map((edge, _))).flatten.find(
+ {
+ case (_, ((x, y), _)) =>
+ visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
+ contains(at.getX() - x, at.getY() - y)
+ }) match {
+ case None => None
+ case Some((edge, (_, index))) => Some((edge, index))
+ }
}
def pressed(at: Point)
{
val c = Transform.pane_to_graph_coordinates(at)
- val l = node(c) match {
- case Some(l) =>
- if (visualizer.Selection(l)) visualizer.Selection() else List(l)
- case None => Nil
- }
+ val l =
+ find_node(c) match {
+ case Some(node) =>
+ if (visualizer.Selection.contains(node)) visualizer.Selection.get()
+ else List(node)
+ case None => Nil
+ }
val d =
l match {
case Nil =>
@@ -231,25 +235,27 @@
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()
{
- (p, m) match {
- case (Some(l), Key.Modifier.Control) => visualizer.Selection.add(l)
+ (find_node(c), m) match {
+ case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
case (None, Key.Modifier.Control) =>
- case (Some(l), Key.Modifier.Shift) => visualizer.Selection.add(l)
+ case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node)
case (None, Key.Modifier.Shift) =>
- case (Some(l), _) => visualizer.Selection.set(List(l))
- case (None, _) => visualizer.Selection.clear
+ case (Some(node), _) =>
+ visualizer.Selection.clear()
+ visualizer.Selection.add(node)
+ case (None, _) =>
+ visualizer.Selection.clear()
}
}
def right_click()
{
- val menu = Popups(panel, p, visualizer.Selection())
+ val menu = Popups(panel, find_node(c), visualizer.Selection.get())
menu.show(panel.peer, at.x, at.y)
}
@@ -259,7 +265,7 @@
}
}
- def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point)
+ def drag(draginfo: (Point, List[Graph_Display.Node], List[Dummy]), to: Point)
{
val (from, p, d) = draginfo
--- a/src/Tools/Graphview/layout.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/layout.scala Sat Jan 03 20:22:27 2015 +0100
@@ -13,23 +13,22 @@
final case class Layout(
nodes: Layout.Coordinates,
- dummies: Map[(Layout.Key, Layout.Key), List[Layout.Point]])
+ dummies: Map[Graph_Display.Edge, List[Layout.Point]])
object Layout
{
- type Key = String
+ type Key = Graph_Display.Node
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 =
+ def make(graph: Graph_Display.Graph, box_distance: Double, box_height: Int => Double): Layout =
{
if (graph.is_empty) empty
else {
@@ -54,9 +53,7 @@
(((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)
+ case ((coords2, x), key) => (coords2 + (key -> (x, y)), x + box_distance)
})._1, y + box_height(level.length))
})._1
@@ -72,18 +69,22 @@
}
- def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies =
+ def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int])
+ : (Graph_Display.Graph, List[Key], Map[Key, Int]) =
{
val ds =
- ((levels(from) + 1) until levels(to))
- .map("%s$%s$%d" format (from, to, _)).toList
+ ((levels(from) + 1) until levels(to)).map(l => {
+ // FIXME !?
+ val ident = "%s$%s$%d".format(from.ident, to.ident, l)
+ Graph_Display.Node(ident, ident)
+ }).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 graph1 = (graph /: ds)(_.new_node(_, Nil))
val graph2 =
(graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
case (g, List(x, y)) => g.add_edge(x, y)
@@ -91,7 +92,7 @@
(graph2, ds, ls)
}
- def level_map(graph: Model.Graph): Map[Key, Int] =
+ def level_map(graph: Graph_Display.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) }
@@ -105,10 +106,10 @@
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
+ buckets.iterator.map(_.sorted(Graph_Display.Node.Ordering)).toList
}
- def count_crossings(graph: Model.Graph, levels: Levels): Int =
+ def count_crossings(graph: Graph_Display.Graph, levels: Levels): Int =
{
def in_level(ls: Levels): Int = ls match {
case List(top, bot) =>
@@ -131,7 +132,7 @@
levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
}
- def minimize_crossings(graph: Model.Graph, levels: Levels): Levels =
+ def minimize_crossings(graph: Graph_Display.Graph, levels: Levels): Levels =
{
def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
child.map(k => {
@@ -165,7 +166,7 @@
}._1
}
- def pendulum(graph: Model.Graph, box_distance: Double,
+ def pendulum(graph: Graph_Display.Graph, box_distance: Double,
levels: Levels, coords: Map[Key, Point]): Coordinates =
{
type Regions = List[List[Region]]
@@ -251,7 +252,7 @@
}._2
}
- private class Region(val graph: Model.Graph, node: Key)
+ private class Region(val graph: Graph_Display.Graph, node: Key)
{
var nodes: List[Key] = List(node)
--- a/src/Tools/Graphview/model.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/model.scala Sat Jan 03 20:22:27 2015 +0100
@@ -33,39 +33,14 @@
}
-object Model
-{
- /* node info */
-
- sealed case class Info(name: String, content: XML.Body)
-
- val empty_info: Info = Info("", Nil)
-
- val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
- {
- import XML.Decode._
-
- val (name, content) = pair(string, x => x)(body)
- Info(name, content)
- }
-
-
- /* graph */
-
- type Graph = isabelle.Graph[String, Info]
-
- val decode_graph: XML.Decode.T[Graph] =
- isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
-}
-
-class Model(val complete_graph: Model.Graph)
+class Model(val complete_graph: Graph_Display.Graph)
{
val Mutators =
new Mutator_Container(
List(
Mutator.Node_Expression(".*", false, false, false),
Mutator.Node_List(Nil, false, false, false),
- Mutator.Edge_Endpoints("", ""),
+ Mutator.Edge_Endpoints(Graph_Display.Node.dummy, Graph_Display.Node.dummy),
Mutator.Add_Node_Expression(""),
Mutator.Add_Transitive_Closure(true, true)))
@@ -75,26 +50,29 @@
Mutator.Node_Expression(".*", false, false, false),
Mutator.Node_List(Nil, false, false, false)))
- def visible_nodes_iterator: Iterator[String] = current_graph.keys_iterator
+ def find_node(ident: String): Option[Graph_Display.Node] =
+ complete_graph.keys_iterator.find(node => node.ident == ident)
- def visible_edges_iterator: Iterator[(String, String)] =
+ def visible_nodes_iterator: Iterator[Graph_Display.Node] = current_graph.keys_iterator
+
+ def visible_edges_iterator: Iterator[Graph_Display.Edge] =
current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))
- def current_graph: Model.Graph =
+ def current_graph: Graph_Display.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]
+ private var _colors = Map.empty[Graph_Display.Node, Color]
def colors = _colors
private def build_colors()
{
_colors =
- (Map.empty[String, Color] /: Colors()) {
+ (Map.empty[Graph_Display.Node, Color] /: Colors()) {
case (colors, m) =>
(colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
- case (colors, k) => colors + (k -> m.color)
+ case (colors, node) => colors + (node -> m.color)
}
}
}
--- a/src/Tools/Graphview/mutator.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala Sat Jan 03 20:22:27 2015 +0100
@@ -24,30 +24,30 @@
class Graph_Filter(
val name: String,
val description: String,
- pred: Model.Graph => Model.Graph) extends Filter
+ pred: Graph_Display.Graph => Graph_Display.Graph) extends Filter
{
- def filter(graph: Model.Graph) : Model.Graph = pred(graph)
+ def filter(graph: Graph_Display.Graph): Graph_Display.Graph = pred(graph)
}
class Graph_Mutator(
val name: String,
val description: String,
- pred: (Model.Graph, Model.Graph) => Model.Graph) extends Mutator
+ pred: (Graph_Display.Graph, Graph_Display.Graph) => Graph_Display.Graph) extends Mutator
{
- def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph =
+ def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph =
pred(complete_graph, graph)
}
class Node_Filter(
name: String,
description: String,
- pred: (Model.Graph, String) => Boolean)
+ pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean)
extends Graph_Filter(name, description, g => g.restrict(pred(g, _)))
class Edge_Filter(
name: String,
description: String,
- pred: (Model.Graph, String, String) => Boolean)
+ pred: (Graph_Display.Graph, Graph_Display.Node, Graph_Display.Node) => Boolean)
extends Graph_Filter(
name,
description,
@@ -63,7 +63,7 @@
reverse: Boolean,
parents: Boolean,
children: Boolean,
- pred: (Model.Graph, String) => Boolean)
+ pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean)
extends Node_Filter(
name,
description,
@@ -90,10 +90,10 @@
reverse,
parents,
children,
- (g, k) => (regex.r findFirstIn k).isDefined)
+ (g, node) => (regex.r findFirstIn node.toString).isDefined)
case class Node_List(
- list: List[String],
+ list: List[Graph_Display.Node],
reverse: Boolean,
parents: Boolean,
children: Boolean)
@@ -103,15 +103,16 @@
reverse,
parents,
children,
- (g, k) => list.exists(_ == k))
+ (g, node) => list.contains(node))
- case class Edge_Endpoints(source: String, dest: String)
+ case class Edge_Endpoints(source: Graph_Display.Node, dest: Graph_Display.Node)
extends Edge_Filter(
"Hide edge",
"Hides the edge whose endpoints match strings.",
(g, s, d) => !(s == source && d == dest))
- private def add_node_group(from: Model.Graph, to: Model.Graph, keys: List[String]) =
+ private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph,
+ keys: List[Graph_Display.Node]) =
{
// Add Nodes
val with_nodes =
@@ -120,7 +121,7 @@
// Add Edges
(with_nodes /: keys) {
(gv, key) => {
- def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
+ def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) =
(g /: keys) {
(graph, end) => {
if (!graph.keys_iterator.contains(end)) graph
@@ -145,7 +146,7 @@
"Adds all relevant edges.",
(complete_graph, graph) =>
add_node_group(complete_graph, graph,
- complete_graph.keys.filter(k => (regex.r findFirstIn k).isDefined).toList))
+ complete_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList))
case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
extends Graph_Mutator(
@@ -165,13 +166,13 @@
{
val name: String
val description: String
- def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph
+ def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.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
+ def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
+ def filter(graph: Graph_Display.Graph): Graph_Display.Graph
}
--- a/src/Tools/Graphview/mutator_dialog.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Sat Jan 03 20:22:27 2015 +0100
@@ -246,6 +246,7 @@
def get_mutator: Mutator.Info =
{
+ val model = visualizer.model
val m =
initials.mutator match {
case Mutator.Identity() =>
@@ -260,15 +261,21 @@
inputs(0)._2.bool)
case Mutator.Node_List(_, _, _, _) =>
Mutator.Node_List(
- inputs(2)._2.string.split(',').filter(_ != "").toList,
+ for {
+ ident <- space_explode(',', inputs(2)._2.string)
+ node <- model.find_node(ident)
+ } yield node,
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)
+ (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match {
+ case (Some(node1), Some(node2)) =>
+ Mutator.Edge_Endpoints(node1, node2)
+ case _ =>
+ Mutator.Identity()
+ }
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)
@@ -295,12 +302,12 @@
List(
("", new Check_Box_Input("Parents", check_children)),
("", new Check_Box_Input("Children", check_parents)),
- ("Names", new Text_Field_Input(list.mkString(","))),
+ ("Names", new Text_Field_Input(list.map(_.ident).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)))
+ ("Source", new Text_Field_Input(source.ident)),
+ ("Destination", new Text_Field_Input(dest.ident)))
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) =>
--- a/src/Tools/Graphview/popups.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/popups.scala Sat Jan 03 20:22:27 2015 +0100
@@ -16,46 +16,50 @@
object Popups
{
- def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]): JPopupMenu =
+ def apply(
+ panel: Graph_Panel,
+ mouse_node: Option[Graph_Display.Node],
+ selected_nodes: List[Graph_Display.Node]): JPopupMenu =
{
val visualizer = panel.visualizer
val add_mutator = visualizer.model.Mutators.add _
val curr = visualizer.model.current_graph
- def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) =
+ def filter_context(
+ nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
new Menu(caption) {
contents +=
new MenuItem(new Action("This") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, false)))
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, false)))
})
contents +=
new MenuItem(new Action("Family") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, true)))
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, true)))
})
contents +=
new MenuItem(new Action("Parents") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, true)))
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, true)))
})
contents +=
new MenuItem(new Action("Children") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, false)))
+ add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false)))
})
if (edges) {
val outs =
- ls.map(l => (l, curr.imm_succs(l))) // FIXME iterator
- .filter(_._2.size > 0).sortBy(_._1)
+ nodes.map(l => (l, curr.imm_succs(l))) // FIXME iterator
+ .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
val ins =
- ls.map(l => (l, curr.imm_preds(l))) // FIXME iterator
- .filter(_._2.size > 0).sortBy(_._1)
+ nodes.map(l => (l, curr.imm_preds(l))) // FIXME iterator
+ .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
if (outs.nonEmpty || ins.nonEmpty) {
contents += new Separator()
@@ -68,13 +72,13 @@
outs.map(e => {
val (from, tos) = e
contents +=
- new Menu(from) {
+ new Menu(from.toString) {
contents += new MenuItem("To...") { enabled = false }
- tos.toList.sorted.distinct.map(to => {
+ tos.toList.sorted(Graph_Display.Node.Ordering).distinct.map(to => {
contents +=
new MenuItem(
- new Action(to) {
+ new Action(to.toString) {
def apply =
add_mutator(
Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
@@ -90,13 +94,13 @@
ins.map(e => {
val (to, froms) = e
contents +=
- new Menu(to) {
+ new Menu(to.toString) {
contents += new MenuItem("From...") { enabled = false }
- froms.toList.sorted.distinct.map(from => {
+ froms.toList.sorted(Graph_Display.Node.Ordering).distinct.map(from => {
contents +=
new MenuItem(
- new Action(from) {
+ new Action(from.toString) {
def apply =
add_mutator(
Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
@@ -114,30 +118,27 @@
popup.add(
new MenuItem(
- new Action("Remove all filters") {
- def apply = visualizer.model.Mutators(Nil)
- }).peer)
+ new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) }).peer)
popup.add(new JPopupMenu.Separator)
- if (under_mouse.isDefined) {
- val v = under_mouse.get
- popup.add(
- new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) { enabled = false }.peer)
+ if (mouse_node.isDefined) {
+ val node = mouse_node.get
+ popup.add(new MenuItem("Mouseover: " + node) { enabled = false }.peer)
- popup.add(filter_context(List(v), true, "Hide", true).peer)
- popup.add(filter_context(List(v), false, "Show only", false).peer)
+ popup.add(filter_context(List(node), true, "Hide", true).peer)
+ popup.add(filter_context(List(node), false, "Show only", false).peer)
popup.add(new JPopupMenu.Separator)
}
- if (!selected.isEmpty) {
+ if (!selected_nodes.isEmpty) {
val text =
- if (selected.length > 1) "Multiple"
- else visualizer.Caption(selected.head)
+ if (selected_nodes.length > 1) "Multiple"
+ else selected_nodes.head.toString
- popup.add(new MenuItem("Selected: %s".format(text)) { enabled = false }.peer)
+ popup.add(new MenuItem("Selected: " + 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(filter_context(selected_nodes, true, "Hide", true).peer)
+ popup.add(filter_context(selected_nodes, false, "Show only", false).peer)
popup.add(new JPopupMenu.Separator)
}
--- a/src/Tools/Graphview/shapes.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Sat Jan 03 20:22:27 2015 +0100
@@ -8,6 +8,8 @@
package isabelle.graphview
+import isabelle._
+
import java.awt.{BasicStroke, Graphics2D, Shape}
import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
@@ -16,8 +18,8 @@
{
trait Node
{
- def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape
- def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
+ def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape
+ def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit
}
object Growing_Node extends Node
@@ -25,24 +27,22 @@
private val stroke =
new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
- def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String])
+ def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
: Rectangle2D.Double =
{
- val (x, y) = visualizer.Coordinates(peer.get)
- val bounds = m.string_bounds(visualizer.Caption(peer.get))
+ val (x, y) = visualizer.Coordinates(node)
+ val bounds = m.string_bounds(node.toString)
val w = bounds.getWidth + m.pad
val h = bounds.getHeight + m.pad
new Rectangle2D.Double((x - (w / 2)).floor, (y - (h / 2)).floor, w.ceil, h.ceil)
}
- def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
+ def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
{
val m = Visualizer.Metrics(g)
- val s = shape(m, visualizer, peer)
- val c = visualizer.node_color(peer)
-
- val caption = visualizer.Caption(peer.get)
- val bounds = m.string_bounds(caption)
+ val s = shape(m, visualizer, node)
+ val c = visualizer.node_color(node)
+ val bounds = m.string_bounds(node.toString)
g.setColor(c.background)
g.fill(s)
@@ -52,7 +52,7 @@
g.draw(s)
g.setColor(c.foreground)
- g.drawString(caption,
+ g.drawString(node.toString,
(s.getCenterX - bounds.getWidth / 2).round.toInt,
(s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt)
}
@@ -64,22 +64,22 @@
new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
private val identity = new AffineTransform()
- def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape =
+ def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape =
{
val w = (m.space_width / 2).ceil
new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
}
- def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
- paint_transformed(g, visualizer, peer, identity)
+ def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit =
+ paint_transformed(g, visualizer, node, identity)
def paint_transformed(g: Graphics2D, visualizer: Visualizer,
- peer: Option[String], at: AffineTransform)
+ node: Graph_Display.Node, at: AffineTransform)
{
val m = Visualizer.Metrics(g)
- val s = shape(m, visualizer, peer)
+ val s = shape(m, visualizer, node)
+ val c = visualizer.node_color(node)
- val c = visualizer.node_color(peer)
g.setStroke(stroke)
g.setColor(c.border)
g.draw(at.createTransformedShape(s))
@@ -88,8 +88,8 @@
trait Edge
{
- def paint(g: Graphics2D, visualizer: Visualizer,
- peer: (String, String), head: Boolean, dummies: Boolean)
+ def paint(g: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge,
+ head: Boolean, dummies: Boolean)
}
object Straight_Edge extends Edge
@@ -98,36 +98,37 @@
new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
def paint(g: Graphics2D, visualizer: Visualizer,
- peer: (String, String), head: Boolean, dummies: Boolean)
+ edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
{
- val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+ val (fx, fy) = visualizer.Coordinates(edge._1)
+ val (tx, ty) = visualizer.Coordinates(edge._2)
val ds =
{
val min = fy min ty
val max = fy max ty
- visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
+ visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
}
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
path.moveTo(fx, fy)
- ds.foreach({case (x, y) => path.lineTo(x, y)})
+ ds.foreach({ case (x, y) => path.lineTo(x, y) })
path.lineTo(tx, ty)
if (dummies) {
ds.foreach({
case (x, y) => {
val at = AffineTransform.getTranslateInstance(x, y)
- Dummy.paint_transformed(g, visualizer, None, at)
+ Dummy.paint_transformed(g, visualizer, Graph_Display.Node.dummy, at)
}
})
}
g.setStroke(stroke)
- g.setColor(visualizer.edge_color(peer))
+ g.setColor(visualizer.edge_color(edge))
g.draw(path)
if (head)
- Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
+ Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), edge._2))
}
}
@@ -138,18 +139,18 @@
private val slack = 0.1
def paint(g: Graphics2D, visualizer: Visualizer,
- peer: (String, String), head: Boolean, dummies: Boolean)
+ edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
{
- val ((fx, fy), (tx, ty)) =
- (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+ val (fx, fy) = visualizer.Coordinates(edge._1)
+ val (tx, ty) = visualizer.Coordinates(edge._2)
val ds =
{
val min = fy min ty
val max = fy max ty
- visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+ visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
}
- if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies)
+ if (ds.isEmpty) Straight_Edge.paint(g, visualizer, edge, head, dummies)
else {
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
path.moveTo(fx, fy)
@@ -178,17 +179,17 @@
ds.foreach({
case (x, y) => {
val at = AffineTransform.getTranslateInstance(x, y)
- Dummy.paint_transformed(g, visualizer, None, at)
+ Dummy.paint_transformed(g, visualizer, Graph_Display.Node.dummy, at)
}
})
}
g.setStroke(stroke)
- g.setColor(visualizer.edge_color(peer))
+ g.setColor(visualizer.edge_color(edge))
g.draw(path)
if (head)
- Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
+ Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), edge._2))
}
}
}
@@ -202,7 +203,7 @@
def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
{
val i = path.getPathIterator(null, 1.0)
- val seg = Array[Double](0,0,0,0,0,0)
+ val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0)
var p1 = (0.0, 0.0)
var p2 = (0.0, 0.0)
while (!i.isDone()) {
--- a/src/Tools/Graphview/visualizer.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Sat Jan 03 20:22:27 2015 +0100
@@ -105,21 +105,18 @@
{
private var layout = Layout.empty
- def apply(k: String): (Double, Double) =
- layout.nodes.getOrElse(k, (0.0, 0.0))
+ def apply(node: Graph_Display.Node): (Double, Double) =
+ layout.nodes.getOrElse(node, (0.0, 0.0))
- def apply(e: (String, String)): List[(Double, Double)] =
- layout.dummies.get(e) match {
- case Some(ds) => ds
- case None => Nil
- }
+ def apply(edge: Graph_Display.Edge): List[(Double, Double)] =
+ layout.dummies.getOrElse(edge, Nil)
- def reposition(k: String, to: (Double, Double))
+ def reposition(node: Graph_Display.Node, to: (Double, Double))
{
- layout = layout.copy(nodes = layout.nodes + (k -> to))
+ layout = layout.copy(nodes = layout.nodes + (node -> to))
}
- def reposition(d: ((String, String), Int), to: (Double, Double))
+ def reposition(d: (Graph_Display.Edge, Int), to: (Double, Double))
{
val (e, index) = d
layout.dummies.get(e) match {
@@ -133,15 +130,15 @@
}
}
- def translate(k: String, by: (Double, Double))
+ def translate(node: Graph_Display.Node, by: (Double, Double))
{
- val ((x, y), (dx, dy)) = (Coordinates(k), by)
- reposition(k, (x + dx, y + dy))
+ val ((x, y), (dx, dy)) = (Coordinates(node), by)
+ reposition(node, (x + dx, y + dy))
}
- def translate(d: ((String, String), Int), by: (Double, Double))
+ def translate(d: (Graph_Display.Edge, Int), by: (Double, Double))
{
- val ((e, i),(dx, dy)) = (d, by)
+ val ((e, i), (dx, dy)) = (d, by)
val (x, y) = apply(e)(i)
reposition(d, (x + dx, y + dy))
}
@@ -154,8 +151,8 @@
val m = metrics()
val max_width =
- model.current_graph.iterator.map({ case (_, (info, _)) =>
- m.string_bounds(info.name).getWidth }).max
+ model.current_graph.keys_iterator.map(
+ node => m.string_bounds(node.toString).getWidth).max
val box_distance = (max_width + m.pad + m.gap).ceil
def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
@@ -170,8 +167,8 @@
var y0 = 0.0
var x1 = 0.0
var y1 = 0.0
- for (node_name <- model.visible_nodes_iterator) {
- val shape = Shapes.Growing_Node.shape(m, visualizer, Some(node_name))
+ for (node <- model.visible_nodes_iterator) {
+ val shape = Shapes.Growing_Node.shape(m, visualizer, node)
x0 = x0 min shape.getMinX
y0 = y0 min shape.getMinY
x1 = x1 max shape.getMaxX
@@ -187,67 +184,46 @@
object Drawer
{
- def apply(g: Graphics2D, n: Option[String])
- {
- n match {
- case None =>
- case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
- }
- }
+ def apply(g: Graphics2D, node: Graph_Display.Node): Unit =
+ if (!node.is_dummy) Shapes.Growing_Node.paint(g, visualizer, node)
- def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
- {
- Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
- }
+ def apply(g: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
+ Shapes.Cardinal_Spline_Edge.paint(g, visualizer, edge, head, dummies)
def paint_all_visible(g: Graphics2D, dummies: Boolean)
{
g.setFont(font)
-
g.setRenderingHints(rendering_hints)
-
- model.visible_edges_iterator.foreach(e => {
- apply(g, e, arrow_heads, dummies)
- })
-
- model.visible_nodes_iterator.foreach(l => {
- apply(g, Some(l))
- })
+ model.visible_edges_iterator.foreach(apply(g, _, arrow_heads, dummies))
+ model.visible_nodes_iterator.foreach(apply(g, _))
}
- def shape(m: Visualizer.Metrics, n: Option[String]): Shape =
- if (n.isEmpty) Shapes.Dummy.shape(m, visualizer, n)
- else Shapes.Growing_Node.shape(m, visualizer, n)
+ def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
+ if (node.is_dummy) Shapes.Dummy.shape(m, visualizer, node)
+ else Shapes.Growing_Node.shape(m, visualizer, node)
}
object Selection
{
- private var selected: List[String] = Nil
+ // owned by GUI thread
+ private var state: List[Graph_Display.Node] = Nil
- def apply() = selected
- def apply(s: String) = selected.contains(s)
+ def get(): List[Graph_Display.Node] = GUI_Thread.require { state }
+ def contains(node: Graph_Display.Node): Boolean = get().contains(node)
- def add(s: String) { selected = s :: selected }
- def set(ss: List[String]) { selected = ss }
- def clear() { selected = Nil }
+ def add(node: Graph_Display.Node): Unit = GUI_Thread.require { state = node :: state }
+ def clear(): Unit = GUI_Thread.require { state = Nil }
}
sealed case class Node_Color(border: Color, background: Color, foreground: Color)
- 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 node_color(node: Graph_Display.Node): Node_Color =
+ if (node.is_dummy)
+ Node_Color(foreground1_color, background_color, foreground_color)
+ else if (Selection.contains(node))
+ Node_Color(foreground_color, selection_color, foreground_color)
+ else
+ Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
- def edge_color(e: (String, String)): Color = foreground_color
-
- object Caption
- {
- def apply(key: String) = model.complete_graph.get_node(key).name
- }
+ def edge_color(edge: Graph_Display.Edge): Color = foreground_color
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/active.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/jEdit/src/active.scala Sat Jan 03 20:22:27 2015 +0100
@@ -41,10 +41,7 @@
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
Future.fork {
val graph =
- Exn.capture {
- isabelle.graphview.Model.decode_graph(body)
- .transitive_reduction_acyclic
- }
+ Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sat Jan 03 20:22:27 2015 +0100
@@ -24,10 +24,10 @@
private var implicit_snapshot = Document.Snapshot.init
- private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
+ private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph"))
private var implicit_graph = no_graph
- private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+ private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
{
GUI_Thread.require {}
@@ -38,7 +38,7 @@
private def reset_implicit(): Unit =
set_implicit(Document.Snapshot.init, no_graph)
- def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+ def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
{
set_implicit(snapshot, graph)
view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")