--- a/src/Pure/build-jars Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Pure/build-jars Wed Jan 28 19:15:13 2015 +0100
@@ -106,6 +106,7 @@
term_xml.scala
"../Tools/Graphview/graph_file.scala"
"../Tools/Graphview/graph_panel.scala"
+ "../Tools/Graphview/graphview.scala"
"../Tools/Graphview/layout.scala"
"../Tools/Graphview/main_panel.scala"
"../Tools/Graphview/metrics.scala"
@@ -116,7 +117,6 @@
"../Tools/Graphview/popups.scala"
"../Tools/Graphview/shapes.scala"
"../Tools/Graphview/tree_panel.scala"
- "../Tools/Graphview/visualizer.scala"
)
--- a/src/Tools/Graphview/graph_file.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/graph_file.scala Wed Jan 28 19:15:13 2015 +0100
@@ -15,9 +15,9 @@
object Graph_File
{
- def write(file: JFile, visualizer: Visualizer)
+ def write(file: JFile, graphview: Graphview)
{
- val box = visualizer.bounding_box()
+ val box = graphview.bounding_box()
val w = box.width.ceil.toInt
val h = box.height.ceil.toInt
@@ -26,7 +26,7 @@
gfx.setColor(Color.WHITE)
gfx.fillRect(0, 0, w, h)
gfx.translate(- box.x, - box.y)
- visualizer.paint_all_visible(gfx)
+ graphview.paint_all_visible(gfx)
}
val name = file.getName
@@ -40,9 +40,9 @@
val model = new Model(graph.transitive_reduction_acyclic)
val the_options = options
- val visualizer = new Visualizer(model) { def options = the_options }
- visualizer.update_layout()
+ val graphview = new Graphview(model) { def options = the_options }
+ graphview.update_layout()
- write(file, visualizer)
+ write(file, graphview)
}
}
--- a/src/Tools/Graphview/graph_panel.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Wed Jan 28 19:15:13 2015 +0100
@@ -20,7 +20,7 @@
import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}
-class Graph_Panel(val visualizer: Visualizer) extends BorderPanel
+class Graph_Panel(val graphview: Graphview) extends BorderPanel
{
graph_panel =>
@@ -36,17 +36,17 @@
{
super.paintComponent(gfx)
- gfx.setColor(visualizer.background_color)
+ gfx.setColor(graphview.background_color)
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
gfx.transform(Transform())
- visualizer.paint_all_visible(gfx)
+ graphview.paint_all_visible(gfx)
}
}
def set_preferred_size()
{
- val box = visualizer.bounding_box()
+ val box = graphview.bounding_box()
val s = Transform.scale_discrete
painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
painter.revalidate()
@@ -62,8 +62,8 @@
def scroll_to_node(node: Graph_Display.Node)
{
- val gap = visualizer.metrics.gap
- val info = visualizer.layout.get_node(node)
+ val gap = graphview.metrics.gap
+ val info = graphview.layout.get_node(node)
val t = Transform()
val p =
@@ -84,12 +84,12 @@
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
override def getToolTipText(event: java.awt.event.MouseEvent): String =
- visualizer.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+ graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
case Some(node) =>
- visualizer.model.full_graph.get_node(node) match {
+ graphview.model.full_graph.get_node(node) match {
case Nil => null
case content =>
- visualizer.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
+ graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
}
case None => null
}
@@ -144,13 +144,13 @@
def scale_discrete: Double =
{
- val font_height = GUI.line_metrics(visualizer.metrics.font).getHeight.toInt
+ val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt
(scale * font_height).floor / font_height
}
def apply() =
{
- val box = visualizer.bounding_box()
+ val box = graphview.bounding_box()
val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
t.translate(- box.x, - box.y)
t
@@ -158,10 +158,10 @@
def fit_to_window()
{
- if (visualizer.visible_graph.is_empty)
+ if (graphview.visible_graph.is_empty)
rescale(1.0)
else {
- val box = visualizer.bounding_box()
+ val box = graphview.bounding_box()
rescale((size.width / box.width) min (size.height / box.height))
}
}
@@ -179,8 +179,8 @@
/* interaction */
- visualizer.model.Colors.events += { case _ => painter.repaint() }
- visualizer.model.Mutators.events += { case _ => painter.repaint() }
+ graphview.model.Colors.events += { case _ => painter.repaint() }
+ graphview.model.Mutators.events += { case _ => painter.repaint() }
private object Mouse_Interaction
{
@@ -191,15 +191,15 @@
{
val c = Transform.pane_to_graph_coordinates(at)
val l =
- visualizer.find_node(c) match {
+ graphview.find_node(c) match {
case Some(node) =>
- if (visualizer.Selection.contains(node)) visualizer.Selection.get()
+ if (graphview.Selection.contains(node)) graphview.Selection.get()
else List(node)
case None => Nil
}
val d =
l match {
- case Nil => visualizer.find_dummy(c).toList
+ case Nil => graphview.find_dummy(c).toList
case _ => Nil
}
draginfo = (at, l, d)
@@ -220,10 +220,10 @@
painter.peer.scrollRectToVisible(r)
case (Nil, ds) =>
- ds.foreach(d => visualizer.translate_vertex(d, dx / s, dy / s))
+ ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s))
case (ls, _) =>
- ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s))
+ ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s))
}
draginfo = (to, p, d)
@@ -237,23 +237,23 @@
if (right_click) {
// FIXME
if (false) {
- val menu = Popups(graph_panel, visualizer.find_node(c), visualizer.Selection.get())
+ val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get())
menu.show(graph_pane.peer, at.x, at.y)
}
}
else {
- (visualizer.find_node(c), m) match {
- case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
+ (graphview.find_node(c), m) match {
+ case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node)
case (None, Key.Modifier.Control) =>
- case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node)
+ case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node)
case (None, Key.Modifier.Shift) =>
case (Some(node), _) =>
- visualizer.Selection.clear()
- visualizer.Selection.add(node)
+ graphview.Selection.clear()
+ graphview.Selection.add(node)
case (None, _) =>
- visualizer.Selection.clear()
+ graphview.Selection.clear()
}
}
}
@@ -265,9 +265,9 @@
/** controls **/
private val mutator_dialog =
- new Mutator_Dialog(visualizer, visualizer.model.Mutators, "Filters", "Hide", false)
+ new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false)
private val color_dialog =
- new Mutator_Dialog(visualizer, visualizer.model.Colors, "Colorations")
+ new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations")
private val chooser = new FileChooser {
fileSelectionMode = FileChooser.SelectionMode.FilesOnly
@@ -275,28 +275,28 @@
}
private val show_content = new CheckBox() {
- selected = visualizer.show_content
+ selected = graphview.show_content
action = Action("Show content") {
- visualizer.show_content = selected
- visualizer.update_layout()
+ graphview.show_content = selected
+ graphview.update_layout()
refresh()
}
tooltip = "Show full node content within graph layout"
}
private val show_arrow_heads = new CheckBox() {
- selected = visualizer.show_arrow_heads
+ selected = graphview.show_arrow_heads
action = Action("Show arrow heads") {
- visualizer.show_arrow_heads = selected
+ graphview.show_arrow_heads = selected
painter.repaint()
}
tooltip = "Draw edges with explicit arrow heads"
}
private val show_dummies = new CheckBox() {
- selected = visualizer.show_dummies
+ selected = graphview.show_dummies
action = Action("Show dummies") {
- visualizer.show_dummies = selected
+ graphview.show_dummies = selected
painter.repaint()
}
tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
@@ -306,7 +306,7 @@
action = Action("Save image") {
chooser.showSaveDialog(this) match {
case FileChooser.Result.Approve =>
- try { Graph_File.write(chooser.selectedFile, visualizer) }
+ try { Graph_File.write(chooser.selectedFile, graphview) }
catch {
case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
}
@@ -325,7 +325,7 @@
private val update_layout = new Button {
action = Action("Update layout") {
- visualizer.update_layout()
+ graphview.update_layout()
refresh()
}
tooltip = "Regenerate graph layout according to built-in algorithm"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/graphview.scala Wed Jan 28 19:15:13 2015 +0100
@@ -0,0 +1,178 @@
+/* Title: Tools/Graphview/graphview.scala
+ Author: Markus Kaiser, TU Muenchen
+ Author: Makarius
+
+Graphview visualization parameters and GUI state.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.{Font, Color, Shape, Graphics2D}
+import java.awt.geom.{Point2D, Rectangle2D}
+import javax.swing.JComponent
+
+
+abstract class Graphview(val model: Model)
+{
+ graphview =>
+
+
+ def options: Options
+
+
+ /* layout state */
+
+ // owned by GUI thread
+ private var _layout: Layout = Layout.empty
+ def layout: Layout = _layout
+
+ def metrics: Metrics = layout.metrics
+ def visible_graph: Graph_Display.Graph = layout.input_graph
+
+ def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
+ _layout = _layout.translate_vertex(v, dx, dy)
+
+ def find_node(at: Point2D): Option[Graph_Display.Node] =
+ layout.output_graph.iterator.collectFirst({
+ case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node
+ })
+
+ def find_dummy(at: Point2D): Option[Layout.Dummy] =
+ layout.output_graph.iterator.collectFirst({
+ case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy
+ })
+
+ def bounding_box(): Rectangle2D.Double =
+ {
+ var x0 = 0.0
+ var y0 = 0.0
+ var x1 = 0.0
+ var y1 = 0.0
+ for ((_, (info, _)) <- layout.output_graph.iterator) {
+ val rect = Shapes.shape(info)
+ x0 = x0 min rect.getMinX
+ y0 = y0 min rect.getMinY
+ x1 = x1 max rect.getMaxX
+ y1 = y1 max rect.getMaxY
+ }
+ x0 = (x0 - metrics.gap).floor
+ y0 = (y0 - metrics.gap).floor
+ x1 = (x1 + metrics.gap).ceil
+ y1 = (y1 + metrics.gap).ceil
+ new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
+ }
+
+ def update_layout()
+ {
+ val metrics = Metrics(make_font())
+ val visible_graph = model.make_visible_graph()
+
+ def node_text(node: Graph_Display.Node, content: XML.Body): String =
+ if (show_content) {
+ val s =
+ XML.content(Pretty.formatted(
+ content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric))
+ if (s.nonEmpty) s else node.toString
+ }
+ else node.toString
+
+ _layout = Layout.make(options, metrics, node_text _, visible_graph)
+ }
+
+
+ /* tooltips */
+
+ def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
+
+
+ /* main colors */
+
+ def foreground_color: Color = Color.BLACK
+ def background_color: Color = Color.WHITE
+ def selection_color: Color = Color.GREEN
+ def highlight_color: Color = Color.YELLOW
+ def error_color: Color = Color.RED
+ def dummy_color: Color = Color.GRAY
+
+
+ /* font rendering information */
+
+ def make_font(): Font =
+ {
+ val family = options.string("graphview_font_family")
+ val size = options.int("graphview_font_size")
+ new Font(family, Font.PLAIN, size)
+ }
+
+
+ /* rendering parameters */
+
+ // owned by GUI thread
+ var show_content = false
+ var show_arrow_heads = false
+ var show_dummies = false
+
+ object Colors
+ {
+ private val filter_colors = List(
+ 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(): Color =
+ {
+ curr = (curr + 1) % filter_colors.length
+ filter_colors(curr)
+ }
+ }
+
+ def paint_all_visible(gfx: Graphics2D)
+ {
+ gfx.setRenderingHints(Metrics.rendering_hints)
+
+ for (node <- graphview.current_node)
+ Shapes.highlight_node(gfx, graphview, node)
+
+ for (edge <- visible_graph.edges_iterator)
+ Shapes.Cardinal_Spline_Edge.paint(gfx, graphview, edge)
+
+ for (node <- visible_graph.keys_iterator)
+ Shapes.paint_node(gfx, graphview, node)
+ }
+
+ var current_node: Option[Graph_Display.Node] = None
+
+ object Selection
+ {
+ private val state = Synchronized(List.empty[Graph_Display.Node])
+
+ def get(): List[Graph_Display.Node] = state.value
+ def contains(node: Graph_Display.Node): Boolean = get().contains(node)
+
+ def add(node: Graph_Display.Node): Unit = state.change(node :: _)
+ def clear(): Unit = state.change(_ => Nil)
+ }
+
+ sealed case class Node_Color(border: Color, background: Color, foreground: Color)
+
+ def node_color(node: Graph_Display.Node): Node_Color =
+ if (Selection.contains(node))
+ Node_Color(foreground_color, selection_color, foreground_color)
+ else if (current_node == Some(node))
+ Node_Color(foreground_color, highlight_color, foreground_color)
+ else
+ Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
+
+ def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color =
+ if (downwards || show_arrow_heads) foreground_color
+ else error_color
+}
\ No newline at end of file
--- a/src/Tools/Graphview/main_panel.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Wed Jan 28 19:15:13 2015 +0100
@@ -13,19 +13,19 @@
import scala.swing.{SplitPane, Orientation}
-class Main_Panel(visualizer: Visualizer) extends SplitPane(Orientation.Vertical)
+class Main_Panel(graphview: Graphview) extends SplitPane(Orientation.Vertical)
{
oneTouchExpandable = true
- val graph_panel = new Graph_Panel(visualizer)
- val tree_panel = new Tree_Panel(visualizer, graph_panel)
+ val graph_panel = new Graph_Panel(graphview)
+ val tree_panel = new Tree_Panel(graphview, graph_panel)
leftComponent = tree_panel
rightComponent = graph_panel
def update_layout()
{
- visualizer.update_layout()
+ graphview.update_layout()
tree_panel.refresh()
graph_panel.refresh()
}
--- a/src/Tools/Graphview/mutator.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala Wed Jan 28 19:15:13 2015 +0100
@@ -18,8 +18,8 @@
{
sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator)
- def make(visualizer: Visualizer, m: Mutator): Info =
- Info(true, visualizer.Colors.next, m)
+ def make(graphview: Graphview, m: Mutator): Info =
+ Info(true, graphview.Colors.next, m)
class Graph_Filter(
val name: String,
--- a/src/Tools/Graphview/mutator_dialog.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Wed Jan 28 19:15:13 2015 +0100
@@ -20,7 +20,7 @@
class Mutator_Dialog(
- visualizer: Visualizer,
+ graphview: Graphview,
container: Mutator_Container,
caption: String,
reverse_caption: String = "Inverse",
@@ -117,7 +117,7 @@
private val add_button = new Button {
action = Action("Add") {
add_panel(
- new Mutator_Panel(Mutator.Info(true, visualizer.Colors.next, mutator_box.selection.item)))
+ new Mutator_Panel(Mutator.Info(true, graphview.Colors.next, mutator_box.selection.item)))
}
}
@@ -246,7 +246,7 @@
def get_mutator: Mutator.Info =
{
- val model = visualizer.model
+ val model = graphview.model
val m =
initials.mutator match {
case Mutator.Identity() =>
@@ -333,7 +333,7 @@
reactions +=
{
case ValueChanged(_) =>
- foreground = if (check(text)) default_foreground else visualizer.error_color
+ foreground = if (check(text)) default_foreground else graphview.error_color
}
def string = text
--- a/src/Tools/Graphview/popups.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/popups.scala Wed Jan 28 19:15:13 2015 +0100
@@ -21,10 +21,10 @@
mouse_node: Option[Graph_Display.Node],
selected_nodes: List[Graph_Display.Node]): JPopupMenu =
{
- val visualizer = graph_panel.visualizer
+ val graphview = graph_panel.graphview
- val add_mutator = visualizer.model.Mutators.add _
- val visible_graph = visualizer.visible_graph
+ val add_mutator = graphview.model.Mutators.add _
+ val visible_graph = graphview.visible_graph
def filter_context(
nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
@@ -32,25 +32,25 @@
contents +=
new MenuItem(new Action("This") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, false)))
+ add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false)))
})
contents +=
new MenuItem(new Action("Family") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, true)))
+ add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true)))
})
contents +=
new MenuItem(new Action("Parents") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, true)))
+ add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true)))
})
contents +=
new MenuItem(new Action("Children") {
def apply =
- add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false)))
+ add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false)))
})
if (edges) {
@@ -80,7 +80,7 @@
new Action(quote(to.toString)) {
def apply =
add_mutator(
- Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
+ Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
})
}
}
@@ -99,7 +99,7 @@
new Action(quote(from.toString)) {
def apply =
add_mutator(
- Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
+ Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
})
}
}
@@ -114,7 +114,7 @@
popup.add(
new MenuItem(
- new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) }).peer)
+ new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer)
popup.add(new JPopupMenu.Separator)
if (mouse_node.isDefined) {
--- a/src/Tools/Graphview/shapes.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala Wed Jan 28 19:15:13 2015 +0100
@@ -23,13 +23,13 @@
def shape(info: Layout.Info): Rectangle2D.Double =
new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)
- def highlight_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
+ def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
{
- val metrics = visualizer.metrics
+ val metrics = graphview.metrics
val extra = metrics.char_width
- val info = visualizer.layout.get_node(node)
+ val info = graphview.layout.get_node(node)
- gfx.setColor(visualizer.highlight_color)
+ gfx.setColor(graphview.highlight_color)
gfx.fill(new Rectangle2D.Double(
info.x - info.width2 - extra,
info.y - info.height2 - extra,
@@ -37,11 +37,11 @@
info.height + 2 * extra))
}
- def paint_node(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
+ def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
{
- val metrics = visualizer.metrics
- val info = visualizer.layout.get_node(node)
- val c = visualizer.node_color(node)
+ val metrics = graphview.metrics
+ val info = graphview.layout.get_node(node)
+ val c = graphview.node_color(node)
val s = shape(info)
gfx.setColor(c.background)
@@ -63,24 +63,24 @@
for (line <- info.lines) { gfx.drawString(line, x, y); y += metrics.height.ceil.toInt }
}
- def paint_dummy(gfx: Graphics2D, visualizer: Visualizer, info: Layout.Info)
+ def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info)
{
gfx.setStroke(default_stroke)
- gfx.setColor(visualizer.dummy_color)
+ gfx.setColor(graphview.dummy_color)
gfx.draw(shape(info))
}
object Straight_Edge
{
- def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
+ def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
{
- val p = visualizer.layout.get_node(edge._1)
- val q = visualizer.layout.get_node(edge._2)
+ val p = graphview.layout.get_node(edge._1)
+ val q = graphview.layout.get_node(edge._2)
val ds =
{
val a = p.y min q.y
val b = p.y max q.y
- visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
+ graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
}
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
@@ -88,13 +88,13 @@
ds.foreach(d => path.lineTo(d.x, d.y))
path.lineTo(q.x, q.y)
- if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
+ if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))
gfx.setStroke(default_stroke)
- gfx.setColor(visualizer.edge_color(edge, p.y < q.y))
+ gfx.setColor(graphview.edge_color(edge, p.y < q.y))
gfx.draw(path)
- if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
+ if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
}
}
@@ -102,18 +102,18 @@
{
private val slack = 0.1
- def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
+ def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
{
- val p = visualizer.layout.get_node(edge._1)
- val q = visualizer.layout.get_node(edge._2)
+ val p = graphview.layout.get_node(edge._1)
+ val q = graphview.layout.get_node(edge._2)
val ds =
{
val a = p.y min q.y
val b = p.y max q.y
- visualizer.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
+ graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList
}
- if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
+ if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge)
else {
val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
path.moveTo(p.x, p.y)
@@ -140,13 +140,13 @@
q.x - slack * dx2, q.y - slack * dy2,
q.x, q.y)
- if (visualizer.show_dummies) ds.foreach(paint_dummy(gfx, visualizer, _))
+ if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _))
gfx.setStroke(default_stroke)
- gfx.setColor(visualizer.edge_color(edge, p.y < q.y))
+ gfx.setColor(graphview.edge_color(edge, p.y < q.y))
gfx.draw(path)
- if (visualizer.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
+ if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q))
}
}
}
--- a/src/Tools/Graphview/tree_panel.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Wed Jan 28 19:15:13 2015 +0100
@@ -19,22 +19,22 @@
import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action}
-class Tree_Panel(val visualizer: Visualizer, graph_panel: Graph_Panel) extends BorderPanel
+class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel
{
/* main actions */
private def selection_action()
{
if (tree != null) {
- visualizer.current_node = None
- visualizer.Selection.clear()
+ graphview.current_node = None
+ graphview.Selection.clear()
val paths = tree.getSelectionPaths
if (paths != null) {
for (path <- paths if path != null) {
path.getLastPathComponent match {
case tree_node: DefaultMutableTreeNode =>
tree_node.getUserObject match {
- case node: Graph_Display.Node => visualizer.Selection.add(node)
+ case node: Graph_Display.Node => graphview.Selection.add(node)
case _ =>
}
case _ =>
@@ -58,7 +58,7 @@
case _ => None
}
action_node.foreach(graph_panel.scroll_to_node(_))
- visualizer.current_node = action_node
+ graphview.current_node = action_node
graph_panel.repaint()
}
}
@@ -111,7 +111,7 @@
private val selection_field_foreground = selection_field.foreground
private val selection_delay =
- GUI_Thread.delay_last(visualizer.options.seconds("editor_input_delay")) {
+ GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
val (pattern, ok) =
selection_field.text match {
case null | "" => (None, true)
@@ -127,7 +127,7 @@
tree.repaint()
}
selection_field.foreground =
- if (ok) selection_field_foreground else visualizer.error_color
+ if (ok) selection_field_foreground else graphview.error_color
}
selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
@@ -149,7 +149,7 @@
def refresh()
{
- val new_nodes = visualizer.visible_graph.topological_order
+ val new_nodes = graphview.visible_graph.topological_order
if (new_nodes != nodes) {
nodes = new_nodes
--- a/src/Tools/Graphview/visualizer.scala Wed Jan 28 08:29:08 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-/* Title: Tools/Graphview/visualizer.scala
- Author: Markus Kaiser, TU Muenchen
- Author: Makarius
-
-Graph visualization parameters and GUI state.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.{Font, Color, Shape, Graphics2D}
-import java.awt.geom.{Point2D, Rectangle2D}
-import javax.swing.JComponent
-
-
-abstract class Visualizer(val model: Model)
-{
- visualizer =>
-
-
- def options: Options
-
-
- /* layout state */
-
- // owned by GUI thread
- private var _layout: Layout = Layout.empty
- def layout: Layout = _layout
-
- def metrics: Metrics = layout.metrics
- def visible_graph: Graph_Display.Graph = layout.input_graph
-
- def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Unit =
- _layout = _layout.translate_vertex(v, dx, dy)
-
- def find_node(at: Point2D): Option[Graph_Display.Node] =
- layout.output_graph.iterator.collectFirst({
- case (Layout.Node(node), (info, _)) if Shapes.shape(info).contains(at) => node
- })
-
- def find_dummy(at: Point2D): Option[Layout.Dummy] =
- layout.output_graph.iterator.collectFirst({
- case (dummy: Layout.Dummy, (info, _)) if Shapes.shape(info).contains(at) => dummy
- })
-
- def bounding_box(): Rectangle2D.Double =
- {
- var x0 = 0.0
- var y0 = 0.0
- var x1 = 0.0
- var y1 = 0.0
- for ((_, (info, _)) <- layout.output_graph.iterator) {
- val rect = Shapes.shape(info)
- x0 = x0 min rect.getMinX
- y0 = y0 min rect.getMinY
- x1 = x1 max rect.getMaxX
- y1 = y1 max rect.getMaxY
- }
- x0 = (x0 - metrics.gap).floor
- y0 = (y0 - metrics.gap).floor
- x1 = (x1 + metrics.gap).ceil
- y1 = (y1 + metrics.gap).ceil
- new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
- }
-
- def update_layout()
- {
- val metrics = Metrics(make_font())
- val visible_graph = model.make_visible_graph()
-
- def node_text(node: Graph_Display.Node, content: XML.Body): String =
- if (show_content) {
- val s =
- XML.content(Pretty.formatted(
- content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric))
- if (s.nonEmpty) s else node.toString
- }
- else node.toString
-
- _layout = Layout.make(options, metrics, node_text _, visible_graph)
- }
-
-
- /* tooltips */
-
- def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
-
-
- /* main colors */
-
- def foreground_color: Color = Color.BLACK
- def background_color: Color = Color.WHITE
- def selection_color: Color = Color.GREEN
- def highlight_color: Color = Color.YELLOW
- def error_color: Color = Color.RED
- def dummy_color: Color = Color.GRAY
-
-
- /* font rendering information */
-
- def make_font(): Font =
- {
- val family = options.string("graphview_font_family")
- val size = options.int("graphview_font_size")
- new Font(family, Font.PLAIN, size)
- }
-
-
- /* rendering parameters */
-
- // owned by GUI thread
- var show_content = false
- var show_arrow_heads = false
- var show_dummies = false
-
- object Colors
- {
- private val filter_colors = List(
- 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(): Color =
- {
- curr = (curr + 1) % filter_colors.length
- filter_colors(curr)
- }
- }
-
- def paint_all_visible(gfx: Graphics2D)
- {
- gfx.setRenderingHints(Metrics.rendering_hints)
-
- for (node <- visualizer.current_node)
- Shapes.highlight_node(gfx, visualizer, node)
-
- for (edge <- visible_graph.edges_iterator)
- Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
-
- for (node <- visible_graph.keys_iterator)
- Shapes.paint_node(gfx, visualizer, node)
- }
-
- var current_node: Option[Graph_Display.Node] = None
-
- object Selection
- {
- private val state = Synchronized(List.empty[Graph_Display.Node])
-
- def get(): List[Graph_Display.Node] = state.value
- def contains(node: Graph_Display.Node): Boolean = get().contains(node)
-
- def add(node: Graph_Display.Node): Unit = state.change(node :: _)
- def clear(): Unit = state.change(_ => Nil)
- }
-
- sealed case class Node_Color(border: Color, background: Color, foreground: Color)
-
- def node_color(node: Graph_Display.Node): Node_Color =
- if (Selection.contains(node))
- Node_Color(foreground_color, selection_color, foreground_color)
- else if (current_node == Some(node))
- Node_Color(foreground_color, highlight_color, foreground_color)
- else
- Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
-
- def edge_color(edge: Graph_Display.Edge, downwards: Boolean): Color =
- if (downwards || show_arrow_heads) foreground_color
- else error_color
-}
\ No newline at end of file
--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Jan 28 19:15:13 2015 +0100
@@ -62,7 +62,7 @@
graph_result match {
case Exn.Res(graph) =>
val model = new isabelle.graphview.Model(graph)
- val visualizer = new isabelle.graphview.Visualizer(model) {
+ val graphview = new isabelle.graphview.Graphview(model) {
def options: Options = PIDE.options.value
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
@@ -86,7 +86,7 @@
override def highlight_color = view.getTextArea.getPainter.getLineHighlightColor
override def error_color = PIDE.options.color_value("error_color")
}
- new isabelle.graphview.Main_Panel(visualizer)
+ new isabelle.graphview.Main_Panel(graphview)
case Exn.Exn(exn) => new TextArea(Exn.message(exn))
}
set_content(graphview)