--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/dockable.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,53 @@
+/* Title: Tools/Graphview/src/dockable.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graphview jEdit dockable.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.jedit._
+
+import scala.actors.Actor._
+import scala.swing.{FileChooser}
+
+import java.io.File
+import org.gjt.sp.jedit.View
+
+
+class Graphview_Dockable(view: View, position: String)
+extends Dockable(view, position)
+{
+ //FIXME: How does the xml get here?
+ val xml: XML.Tree =
+ try {
+ val chooser = new FileChooser()
+ val path: File = chooser.showOpenDialog(null) match {
+ case FileChooser.Result.Approve =>
+ chooser.selectedFile
+ case _ => new File("~/local_deps.graph")
+ }
+ YXML.parse_body(Symbol.decode(io.Source.fromFile(path).mkString)).head
+ } catch {
+ case ex: Exception => System.err.println(ex.getMessage); null
+ }
+
+
+ set_content(new Main_Panel(xml))
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case result: Isabelle_Process.Output =>
+ case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init() { }
+ override def exit() { }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/floating_dialog.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,43 @@
+/* Title: Tools/Graphview/src/floating_dialog.scala
+ Author: Markus Kaiser, TU Muenchen
+
+PopUp Dialog containing node meta-information.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.jedit._
+
+import scala.swing.{Dialog, BorderPanel, Component}
+import java.awt.{Point, Dimension}
+
+
+class Floating_Dialog(private val html: String, _title: String, _location: Point)
+extends Dialog
+{
+ location = _location
+ title = _title
+ //No adaptive size because we don't want to resize the Dialog about 1 sec
+ //after it is shown.
+ preferredSize = new Dimension(300, 300)
+ peer.setAlwaysOnTop(true)
+
+ private def render_document(text: String) =
+ html_panel.peer.render_document("http://localhost", text)
+
+ private val html_panel = new Component()
+ {
+ override lazy val peer: HTML_Panel =
+ new HTML_Panel(Parameters.font_family, Parameters.font_size) with SuperMixin
+ {
+ setPreferredWidth(290)
+ }
+ }
+
+ render_document(html)
+ contents = new BorderPanel {
+ add(html_panel, BorderPanel.Position.Center)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/frame.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,61 @@
+/* Title: Tools/Graphview/src/frame.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graphview standalone frame.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Dimension
+import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
+import javax.swing.border.EmptyBorder
+
+
+object Graphview_Frame extends SwingApplication
+{
+ def startup(args : Array[String])
+ {
+ try {
+ Platform.init_laf()
+ Isabelle_System.init()
+ }
+ catch { case exn: Throwable => println(Exn.message(exn)); System.exit(1) }
+
+ val opt_xml: Option[XML.Tree] =
+ try {
+ Some(YXML.parse_body(
+ Symbol.decode(io.Source.fromFile(args(0)).mkString)).head)
+ } catch {
+ case _ : ArrayIndexOutOfBoundsException => None
+ case _ : java.io.FileNotFoundException => None
+ }
+
+ //Textfiles will still be valid and result in an empty frame
+ //since they are valid to YXML.
+ opt_xml match {
+ case None =>
+ println("No valid YXML-File given.\n" +
+ "Usage: java -jar graphview.jar <yxmlfile>")
+ System.exit(1)
+ case Some(xml) =>
+ val top = frame(xml)
+ top.pack()
+ top.visible = true
+ }
+
+ def frame(xml: XML.Tree): Window = new MainFrame {
+ title = "Graphview"
+ minimumSize = new Dimension(640, 480)
+ preferredSize = new Dimension(800, 600)
+
+ contents = new BorderPanel {
+ border = new EmptyBorder(5, 5, 5, 5)
+
+ add(new Main_Panel(xml), BorderPanel.Position.Center)
+ }
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/graph_panel.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,319 @@
+/* Title: Tools/Graphview/src/graph_panel.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graphview Java2D drawing panel.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.{Dimension, Graphics2D, Point, Rectangle}
+import java.awt.geom.{AffineTransform, Point2D}
+import javax.swing.ToolTipManager
+import scala.swing.{Panel, ScrollPane}
+import scala.swing.event._
+
+
+class Graph_Panel(private val vis: Visualizer) extends ScrollPane {
+ this.peer.setWheelScrollingEnabled(false)
+ focusable = true
+ requestFocus()
+
+ horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+ verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+
+ def visualizer = vis
+
+ def fit_to_window() = {
+ Transform.fit_to_window()
+ repaint()
+ }
+
+ def apply_layout() = vis.Coordinates.layout()
+
+ private val paint_panel = new Panel {
+ def set_preferred_size() {
+ val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+ val s = Transform.scale
+ val (px, py) = Transform.padding
+
+ preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt,
+ (math.abs(maxY - minY + py) * s).toInt)
+
+ revalidate()
+ }
+
+ override def paint(g: Graphics2D) {
+ set_preferred_size()
+ super.paintComponent(g)
+ g.transform(Transform())
+
+ vis.Drawer.paint_all_visible(g, true)
+ }
+ }
+ contents = paint_panel
+
+ listenTo(keys)
+ listenTo(mouse.moves)
+ listenTo(mouse.clicks)
+ listenTo(mouse.wheel)
+ reactions += Interaction.Mouse.react
+ reactions += Interaction.Keyboard.react
+ reactions += {
+ case KeyTyped(_, _, _, _) => {repaint(); requestFocus()}
+ case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()}
+ case MouseDragged(_, _, _) => {repaint(); requestFocus()}
+ case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()}
+ case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
+ case MouseMoved(_, _, _) => repaint()
+ }
+ private val r = {
+ import scala.actors.Actor._
+
+ actor {
+ loop {
+ react {
+ // FIXME Swing thread!?
+ case _ => repaint()
+ }
+ }
+ }
+ }
+ vis.model.Colors.events += r
+ vis.model.Mutators.events += r
+ ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
+
+ apply_layout()
+ fit_to_window()
+
+ protected object Transform {
+ val padding = (4000, 2000)
+
+ private var _scale = 1d
+ def scale = _scale
+ def scale_= (s: Double) = {
+ _scale = math.max(math.min(s, 10), 0.01)
+ paint_panel.set_preferred_size()
+ }
+
+ def apply() = {
+ val (minX, minY, _, _) = vis.Coordinates.bounds()
+
+ val at = AffineTransform.getScaleInstance(scale, scale)
+ at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
+ at
+ }
+
+ def fit_to_window() {
+ if (vis.model.visible_nodes().isEmpty)
+ scale = 1
+ else {
+ val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+
+ val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
+ val (sx, sy) = (1d * size.width / dx, 1d * size.height / dy)
+ scale = math.min(sx, sy)
+ }
+ }
+
+ def pane_to_graph_coordinates(at: Point2D): Point2D = {
+ val s = Transform.scale
+ val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
+
+ p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
+ p
+ }
+ }
+
+ private val panel = this
+ object Interaction {
+ object Keyboard {
+ import scala.swing.event.Key._
+
+ val react: PartialFunction[Event, Unit] = {
+ case KeyTyped(_, c, m, _) => typed(c, m)
+ }
+
+ def typed(c: Char, m: Modifiers) = (c, m) match {
+ case ('+', _) => {
+ Transform.scale *= 5d/4
+ }
+
+ case ('-', _) => {
+ Transform.scale *= 4d/5
+ }
+
+ case ('0', _) => {
+ Transform.fit_to_window()
+ }
+
+ case('1', _) => {
+ vis.Coordinates.layout()
+ }
+
+ case('2', _) => {
+ Transform.fit_to_window()
+ }
+
+ case _ =>
+ }
+ }
+
+ object Mouse {
+ import java.awt.image.BufferedImage
+ import scala.swing.event.Key.Modifier._
+ type Modifiers = Int
+ type Dummy = ((String, String), Int)
+
+ private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
+ private val g =
+ new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
+ g.setFont(vis.Font())
+ g.setRenderingHints(vis.rendering_hints)
+
+ val react: PartialFunction[Event, Unit] = {
+ case MousePressed(_, p, _, _, _) => pressed(p)
+ case MouseDragged(_, to, _) => {
+ drag(draginfo, to)
+ val (_, p, d) = draginfo
+ draginfo = (to, p, d)
+ }
+ case MouseWheelMoved(_, p, _, r) => wheel(r, p)
+ case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
+ case MouseMoved(_, p, _) => moved(p)
+ }
+
+ def node(at: Point2D): Option[String] =
+ vis.model.visible_nodes().find({
+ l => vis.Drawer.shape(g, Some(l)).contains(at)
+ })
+
+ def dummy(at: Point2D): Option[Dummy] =
+ vis.model.visible_edges().map({
+ i => vis.Coordinates(i).zipWithIndex.map((i, _))
+ }).flatten.find({
+ case (_, ((x, y), _)) =>
+ vis.Drawer.shape(g, None).contains(at.getX() - x, at.getY() - y)
+ }) match {
+ case None => None
+ case Some((name, (_, index))) => Some((name, index))
+ }
+
+ def moved(at: Point) {
+ val c = Transform.pane_to_graph_coordinates(at)
+ node(c) match {
+ case Some(l) => panel.tooltip = vis.Tooltip(l, g.getFontMetrics)
+ case None => panel.tooltip = null
+ }
+ }
+
+ def pressed(at: Point) {
+ val c = Transform.pane_to_graph_coordinates(at)
+ val l = node(c) match {
+ case Some(l) => if (vis.Selection(l))
+ vis.Selection()
+ else
+ List(l)
+
+ case None => Nil
+ }
+ val d = l match {
+ case Nil => dummy(c) match {
+ case Some(d) => List(d)
+ case None => Nil
+ }
+
+ case _ => Nil
+ }
+
+ draginfo = (at, l, d)
+ }
+
+ def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) {
+ import javax.swing.SwingUtilities
+
+ val c = Transform.pane_to_graph_coordinates(at)
+ val p = node(c)
+
+ def left_click() {
+ (p, m) match {
+ case (Some(l), Control) => vis.Selection.add(l)
+ case (None, Control) =>
+
+ case (Some(l), Shift) => vis.Selection.add(l)
+ case (None, Shift) =>
+
+ case (Some(l), _) => vis.Selection.set(List(l))
+ case (None, _) => vis.Selection.clear
+ }
+ }
+
+ def right_click() {
+ val menu = Popups(panel, p, vis.Selection())
+ menu.show(panel.peer, at.x, at.y)
+ }
+
+ def double_click() {
+ p match {
+ case Some(l) => {
+ val p = at.clone.asInstanceOf[Point]
+ SwingUtilities.convertPointToScreen(p, panel.peer)
+ new Floating_Dialog(
+ vis.Tooltip(l, g.getFontMetrics()),
+ vis.Caption(l),
+ at
+ ).open
+ }
+
+ case None =>
+ }
+ }
+
+ if (clicks < 2) {
+ if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
+ else left_click()
+ } else if (clicks == 2) {
+ if (SwingUtilities.isLeftMouseButton(e.peer)) double_click()
+ }
+ }
+
+ def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) {
+ val (from, p, d) = draginfo
+
+ val s = Transform.scale
+ val (dx, dy) = (to.x - from.x, to.y - from.y)
+ (p, d) match {
+ case (Nil, Nil) => {
+ val r = panel.peer.getViewport.getViewRect
+ r.translate(-dx, -dy)
+
+ paint_panel.peer.scrollRectToVisible(r)
+ }
+
+ case (Nil, ds) =>
+ ds.foreach(d => vis.Coordinates.translate(d, (dx / s, dy / s)))
+
+ case (ls, _) =>
+ ls.foreach(l => vis.Coordinates.translate(l, (dx / s, dy / s)))
+ }
+ }
+
+ def wheel(rotation: Int, at: Point) {
+ val at2 = Transform.pane_to_graph_coordinates(at)
+ // > 0 -> up
+ Transform.scale *= (if (rotation > 0) 4d/5 else 5d/4)
+
+ // move mouseposition to center
+ Transform().transform(at2, at2)
+ val r = panel.peer.getViewport.getViewRect
+ val (width, height) = (r.getWidth, r.getHeight)
+ paint_panel.peer.scrollRectToVisible(
+ new Rectangle((at2.getX() - width / 2).toInt,
+ (at2.getY() - height / 2).toInt,
+ width.toInt,
+ height.toInt)
+ )
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/graph_xml.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,74 @@
+/* Title: Tools/Graphview/src/graph_xml.scala
+ Author: Markus Kaiser, TU Muenchen
+
+XML to graph conversion.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+
+case class Locale(val axioms: List[XML.Body], val parameters: List[(String, XML.Body)])
+
+object Graph_XML
+{
+ type Entry = Option[Locale]
+ type Nodes = List[(String, (Entry, List[String]))]
+
+ def apply(xml: XML.Tree): Graph[String, Entry] = {
+ val nodes : Nodes =
+ {
+ try {
+ xml match {
+ case XML.Elem(Markup("thy_deps", Nil), ts) => thy_deps(ts)
+ case XML.Elem(Markup("locale_deps", Nil), ts) => locale_deps(ts)
+ case _ => Nil
+ }
+ }
+ }
+
+ // Add nodes
+ val node_graph =
+ (Graph.string[Entry] /: nodes) {
+ case (graph, (key, (info, _))) => graph.new_node(key, info)
+ }
+
+ // Add edges
+ (node_graph /: nodes) {
+ case (graph, (from, (_, tos))) =>
+ (graph /: tos) {
+ (graph, to) => graph.add_edge(from, to)
+ }
+ }
+ }
+
+ private def thy_deps(ts: XML.Body) : Nodes = {
+ val strings : List[(String, List[String])] = {
+ import XML.Decode._
+
+ list(pair(string, list(string)))(ts)
+ }
+
+ strings.map({case (key, tos) => (key, (None, tos))})
+ }
+
+ private def locale_deps(ts: XML.Body) : Nodes = {
+ // Identity functions return (potential) term-xmls
+ val strings = {
+ import XML.Decode._
+ val node = pair(list(x=>x),pair(list(pair(string,x=>x)),list(list(x=>x))))
+ val graph = list(pair(pair(string, node), list(string)))
+ def symtab[A](f: T[A]) = list(pair(x=>x, f))
+ val dependencies = symtab(symtab(list(list(x=>x))))
+ pair(graph, dependencies)(ts)
+ }
+
+ strings._1.map({
+ case ((key, (axioms, (parameters, _))), tos) =>
+ (key, (Some(Locale(axioms, parameters)), tos))
+ }
+ )
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/layout_pendulum.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,289 @@
+/* Title: Tools/Graphview/src/layout_pendulum.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Pendulum DAG layout algorithm.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+
+object Layout_Pendulum {
+ type Key = String
+ type Entry = Option[Locale]
+ type Point = (Double, Double)
+ type Coordinates = Map[Key, Point]
+ type Level = List[Key]
+ type Levels = List[Level]
+ type Layout = (Coordinates, Map[(Key, Key), List[Point]])
+ type Dummies = (Graph[Key, Entry], List[Key], Map[Key, Int])
+
+ val x_distance = 350
+ val y_distance = 350
+ val pendulum_iterations = 10
+
+ def apply(graph: Graph[Key, Entry]): Layout = {
+ if (graph.entries.isEmpty)
+ (Map[Key, Point](), Map[(Key, Key), List[Point]]())
+ else {
+ val (dummy_graph, dummies, dummy_levels) = {
+ val initial_levels = level_map(graph)
+
+ def add_dummies(graph: Graph[Key, Entry], 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 next_nodes =
+ (graph /: ds) {
+ (graph, d) => graph.new_node(d, None)
+ }
+
+ val next =
+ (next_nodes.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
+ case (graph, List(f, t)) => graph.add_edge(f, t)
+ }
+ (next, ds, ls)
+ }
+
+ ((graph, Map[(Key, Key), List[Key]](), initial_levels) /: graph.keys) {
+ 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 add_dummies(graph, from, to, levels) match {
+ case (next, ds, ls) => (next, dummies + ((from, to) -> ds), ls)
+ }
+ }
+ }
+ }
+ }
+ }
+
+ val levels =
+ minimize_crossings(
+ dummy_graph,
+ level_list(dummy_levels)
+ )
+
+ val coords =
+ pendulum(dummy_graph,
+ levels,
+ initial_coordinates(levels)
+ )
+
+ val dummy_coords =
+ (Map[(Key, Key), List[Point]]() /: dummies.keys) {
+ case (map, key) => map + (key -> dummies(key).map(coords(_)))
+ }
+
+ (coords, dummy_coords)
+ }
+ }
+
+ def level_map(graph: Graph[Key, Entry]): Map[Key, Int] =
+ (Map[Key, Int]() /: graph.topological_order){
+ (levels, key) => {
+ val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
+ levels + (key -> (pred_levels.max + 1))
+ }}
+
+ def level_list(map: Map[Key, Int]): Levels =
+ (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
+ case ((key, i), list) => {
+ if (list.isEmpty) (i, List(key)) :: list
+ else {
+ val (j, l) = list.head
+ if (i == j) (i, key :: l) :: list.tail
+ else (i, List(key)) :: list
+ }
+ }
+ }.map(_._2)
+
+ def count_crossings(graph: Graph[Key, Entry], levels: Levels): Int = {
+ def in_level(ls: Levels): Int = ls match {
+ case List(top, bot) =>
+ top.zipWithIndex.map{
+ case (outer_parent, outer_parent_index) =>
+ graph.imm_succs(outer_parent).map(bot.indexOf(_))
+ .map(outer_child => {
+ (0 until outer_parent_index)
+ .map(inner_parent =>
+ graph.imm_succs(top(inner_parent))
+ .map(bot.indexOf(_))
+ .filter(inner_child => outer_child < inner_child)
+ .size
+ ).sum
+ }).sum
+ }.sum
+
+ case _ => 0
+ }
+
+ levels.sliding(2).map(in_level).sum
+ }
+
+ def minimize_crossings(graph: Graph[Key, Entry], 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 =
+ (0d /: ps) {
+ (w, p) => w + math.max(0, parent.indexOf(p))
+ } / math.max(ps.size, 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 40)) {
+ 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 initial_coordinates(levels: Levels): Coordinates =
+ (Map[Key, Point]() /: levels.reverse.zipWithIndex){
+ case (coords, (level, yi)) =>
+ (coords /: level.zipWithIndex) {
+ case (coords, (node, xi)) =>
+ coords + (node -> (xi * x_distance, yi * y_distance))
+ }
+ }
+
+ def pendulum(graph: Graph[Key, Entry],
+ 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[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) <= x_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)
+ math.max( -(r.distance(coords, prev) - x_distance), d )
+ }
+ else {
+ val next = level(i+1)
+ math.min( r.distance(coords, next) - x_distance, 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
+ }
+
+ protected class Region(val graph: Graph[Key, Entry], 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.min(math.abs(left(coords) - to.left(coords)),
+ 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
+ else graph.imm_succs(k).toList))
+ .map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
+ .sum / nodes.length
+
+ def move(coords: Coordinates, by: Double): Coordinates =
+ (coords /: nodes) {
+ (cs, node) => {
+ val (x, y) = cs(node)
+ cs + (node -> (x + by, y))
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/main_panel.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,133 @@
+/* Title: Tools/Graphview/src/main_panel.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graph Panel wrapper.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import scala.collection.JavaConversions._
+import scala.swing.{BorderPanel, Button, BoxPanel,
+ Orientation, Swing, CheckBox, Action, FileChooser}
+import javax.swing.border.EmptyBorder
+import java.awt.Dimension
+import java.io.File
+
+
+class Main_Panel(xml: XML.Tree) extends BorderPanel
+{
+ focusable = true
+ requestFocus()
+
+ val model = new Model(Graph_XML(xml))
+ val visualizer = new Visualizer(model)
+ val graph_panel = new Graph_Panel(visualizer)
+
+ listenTo(keys)
+ reactions += graph_panel.reactions
+
+ val mutator_dialog = new Mutator_Dialog(
+ model.Mutators,
+ "Filters",
+ "Hide",
+ false
+ )
+
+ val color_dialog = new Mutator_Dialog(
+ model.Colors,
+ "Colorations"
+ )
+
+ private val chooser = new FileChooser()
+ chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
+ chooser.title = "Graph export"
+
+ val options_panel = new BoxPanel(Orientation.Horizontal) {
+ border = new EmptyBorder(0, 0, 10, 0)
+
+ contents += Swing.HGlue
+ contents += new CheckBox(){
+ selected = Parameters.arrow_heads
+ action = Action("Arrow Heads"){
+ Parameters.arrow_heads = selected
+ graph_panel.repaint()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new CheckBox(){
+ selected = Parameters.long_names
+ action = Action("Long Names"){
+ Parameters.long_names = selected
+ graph_panel.repaint()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Save as PNG"){
+ chooser.showSaveDialog(this) match {
+ case FileChooser.Result.Approve => {
+ export(chooser.selectedFile)
+ }
+
+ case _ =>
+ }
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Apply Layout"){
+ graph_panel.apply_layout()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Fit to Window"){
+ graph_panel.fit_to_window()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Colorations"){
+ color_dialog.open
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Filters"){
+ mutator_dialog.open
+ }
+ }
+ }
+
+ add(graph_panel, BorderPanel.Position.Center)
+ add(options_panel, BorderPanel.Position.North)
+
+ private def export(file: File) {
+ import java.awt.image.BufferedImage
+ import javax.imageio.ImageIO
+ import java.awt.geom.Rectangle2D
+ import java.awt.Color
+
+ val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
+ val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
+ (math.abs(maxY - minY) + 200).toInt,
+ BufferedImage.TYPE_INT_RGB)
+ val g = img.createGraphics
+ g.setColor(Color.WHITE)
+ g.fill(new Rectangle2D.Double(0, 0, img.getWidth(), img.getHeight()))
+
+ g.translate(- minX + 200, - minY + 100)
+ visualizer.Drawer.paint_all_visible(g, false)
+ g.dispose()
+
+ try {
+ ImageIO.write(img, "png", file)
+ } catch {
+ case ex: Exception => ex.printStackTrace
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/model.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,87 @@
+/* Title: Tools/Graphview/src/model.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Internal graph representation.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+import java.awt.Color
+import scala.actors.Actor
+import scala.actors.Actor._
+
+
+class Mutator_Container(val available: List[Mutator[String, Option[Locale]]]) {
+ type Mutator_Markup = (Boolean, Color, Mutator[String, Option[Locale]])
+
+ val events = new Event_Bus[Mutator_Event.Message]
+
+ private var _mutators : List[Mutator_Markup] = Nil
+ def apply() = _mutators
+ def apply(mutators: List[Mutator_Markup]){
+ _mutators = mutators
+
+ events.event(Mutator_Event.NewList(mutators))
+ }
+
+ def add(mutator: Mutator_Markup) = {
+ _mutators = _mutators ::: List(mutator)
+
+ events.event(Mutator_Event.Add(mutator))
+ }
+}
+
+class Model(private val graph: Graph[String, Option[Locale]]) {
+ val Mutators = new Mutator_Container(
+ List(
+ Node_Expression(".*", false, false, false),
+ Node_List(Nil, false, false, false),
+ Edge_Endpoints("", ""),
+ Edge_Transitive(),
+ 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[String] = current.keys
+
+ def visible_edges(): Iterator[(String, String)] =
+ current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
+
+ def complete = graph
+ def current: Graph[String, Option[Locale]] =
+ (graph /: Mutators()) {
+ case (g, (enabled, _, mutator)) => {
+ if (!enabled) g
+ else mutator.mutate(graph, g)
+ }
+ }
+
+ private var _colors = Map[String, Color]()
+ def colors = _colors
+
+ private def build_colors() {
+ (Map[String, Color]() /: Colors()) ({
+ case (colors, (enabled, color, mutator)) => {
+ (colors /: mutator.mutate(graph, graph).keys) ({
+ case (colors, k) => colors + (k -> color)
+ })
+ }
+ })
+ }
+ Colors.events += actor {
+ loop {
+ react {
+ case _ => build_colors()
+ }
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,214 @@
+/* Title: Tools/Graphview/src/mutator.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Filters and add-operations on graphs.
+*/
+
+package isabelle.graphview
+
+
+import isabelle.Graph
+import java.awt.Color
+import scala.collection.immutable.SortedSet
+
+
+trait Mutator[Key, Entry]
+{
+ val name: String
+ val description: String
+ def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry]
+
+ override def toString() = name
+}
+
+trait Filter[Key, Entry]
+extends Mutator[Key, Entry]
+{
+ def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]) = filter(sub)
+ def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry]
+}
+
+object Mutators {
+ type Key = String
+ type Entry = Option[Locale]
+ type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
+
+ val Enabled = true
+ val Disabled = false
+
+ def create(m: Mutator[Key, Entry]): Mutator_Markup =
+ (Mutators.Enabled, Parameters.Colors.next, m)
+
+ class Graph_Filter[Key, Entry](val name: String, val description: String,
+ pred: Graph[Key, Entry] => Graph[Key, Entry])
+ extends Filter[Key, Entry]
+ {
+ def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry] = pred(sub)
+ }
+
+ class Graph_Mutator[Key, Entry](val name: String, val description: String,
+ pred: (Graph[Key, Entry], Graph[Key, Entry]) => Graph[Key, Entry])
+ extends Mutator[Key, Entry]
+ {
+ def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry] =
+ pred(complete, sub)
+ }
+
+ class Node_Filter[Key, Entry](name: String, description: String,
+ pred: (Graph[Key, Entry], Key) => Boolean)
+ extends Graph_Filter[Key, Entry] (
+
+ name,
+ description,
+ g => g.restrict(pred(g, _))
+ )
+
+ class Edge_Filter[Key, Entry](name: String, description: String,
+ pred: (Graph[Key, Entry], Key, Key) => Boolean)
+ extends Graph_Filter[Key, Entry] (
+
+ name,
+ description,
+ g => (g /: g.dest) {
+ (graph, k) => {
+ val (from, tos) = k
+ (graph /: tos) {
+ (gr, to) => if (pred(gr, from, to)) gr
+ else gr.del_edge(from, to)
+ }
+ }
+ }
+ )
+
+ class Node_Family_Filter[Key, Entry](name: String, description: String,
+ reverse: Boolean, parents: Boolean, children: Boolean,
+ pred: (Graph[Key, Entry], Key) => Boolean)
+ extends Node_Filter[Key, Entry](
+
+ 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[Key, Entry](
+
+ "Identity",
+ "Does not change the graph.",
+ g => g
+ )
+
+ case class Node_Expression(regex: String,
+ reverse: Boolean, parents: Boolean, children: Boolean)
+ extends Node_Family_Filter[Key, Entry](
+
+ "Filter by Name",
+ "Only shows or hides all nodes with any family member's name matching " +
+ "a regex.",
+ reverse,
+ parents,
+ children,
+ (g, k) => (regex.r findFirstIn k).isDefined
+ )
+
+ case class Node_List(list: List[String],
+ reverse: Boolean, parents: Boolean, children: Boolean)
+ extends Node_Family_Filter[Key, Entry](
+
+ "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[Key, Entry](
+
+ "Hide edge",
+ "Hides the edge whose endpoints match strings.",
+ (g, s, d) => !(s == source && d == dest)
+ )
+
+ case class Edge_Transitive()
+ extends Edge_Filter[Key, Entry](
+
+ "Hide transitive edges",
+ "Hides all transitive edges.",
+ (g, s, d) => {
+ !g.imm_succs(s).filter(_ != d)
+ .exists(p => !(g.irreducible_paths(p, d).isEmpty))
+ }
+ )
+
+ private def add_node_group(from: Graph[Key, Entry], to: Graph[Key, Entry],
+ keys: List[Key]) = {
+
+ // Add Nodes
+ val with_nodes =
+ (to /: keys) {
+ (graph, key) => graph.default_node(key, from.get_node(key))
+ }
+
+ // Add Edges
+ (with_nodes /: keys) {
+ (gv, key) => {
+ def add_edges(g: Graph[Key, Entry], keys: SortedSet[Key], succs: Boolean) =
+ (g /: keys) {
+ (graph, end) => {
+ if (!graph.keys.contains(end)) graph
+ else {
+ if (succs) graph.add_edge(key, end)
+ else graph.add_edge(end, key)
+ }
+ }
+ }
+
+
+ add_edges(
+ add_edges(gv, from.imm_preds(key), false),
+ from.imm_succs(key), true
+ )
+ }
+ }
+ }
+
+ case class Add_Node_Expression(regex: String)
+ extends Graph_Mutator[Key, Entry](
+
+ "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[Key, Entry](
+
+ "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.toList))
+ else
+ sub
+
+ if (children)
+ add_node_group(complete, withparents,
+ complete.all_succs(sub.keys.toList))
+ else
+ withparents
+ }
+ )
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,434 @@
+/* Title: Tools/Graphview/src/mutator_dialog.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Mutator selection and configuration dialog.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.Color
+import java.awt.FocusTraversalPolicy
+import javax.swing.JColorChooser
+import javax.swing.border.EmptyBorder
+import scala.collection.JavaConversions._
+import scala.swing._
+import scala.actors.Actor
+import scala.actors.Actor._
+import isabelle.graphview.Mutators._
+import scala.swing.event.ValueChanged
+
+
+class Mutator_Dialog(
+ container: Mutator_Container, caption: String,
+ reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
+extends Dialog
+{
+ type Key = String
+ type Entry = Option[Locale]
+ type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
+
+ title = caption
+
+ private var _panels: List[Mutator_Panel] = Nil
+ private def panels = _panels
+ private def panels_= (panels: List[Mutator_Panel]) {
+ _panels = panels
+ paintPanels
+ }
+
+ container.events += actor {
+ loop {
+ react {
+ case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+ case Mutator_Event.NewList(ms) => {
+ panels = getPanels(ms)
+ }
+ }
+ }
+ }
+
+ override def open() {
+ if (!visible)
+ panels = getPanels(container())
+
+ super.open
+ }
+
+ minimumSize = new Dimension(700, 200)
+ preferredSize = new Dimension(1000, 300)
+ peer.setFocusTraversalPolicy(focusTraversal)
+
+ private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] =
+ m.filter(_ match {case (_, _, Identity()) => false; case _ => true})
+ .map(m => new Mutator_Panel(m))
+
+ private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] =
+ panels.map(panel => panel.get_Mutator_Markup)
+
+ private def movePanelUp(m: Mutator_Panel) = {
+ def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+ case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
+ case _ => l
+ }
+
+ panels = moveUp(panels)
+ }
+
+ private def movePanelDown(m: Mutator_Panel) = {
+ def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+ case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
+ case _ => l
+ }
+
+ panels = moveDown(panels)
+ }
+
+ private def removePanel(m: Mutator_Panel) = {
+ panels = panels.filter(_ != m).toList
+ }
+
+ private def addPanel(m: Mutator_Panel) = {
+ panels = panels ::: List(m)
+ }
+
+ def paintPanels = {
+ focusTraversal.clear
+ filterPanel.contents.clear
+ panels.map(x => {
+ filterPanel.contents += x
+ focusTraversal.addAll(x.focusList)
+ })
+ filterPanel.contents += Swing.VGlue
+
+ focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component])
+ focusTraversal.add(addButton.peer)
+ focusTraversal.add(applyButton.peer)
+ focusTraversal.add(cancelButton.peer)
+ filterPanel.revalidate
+ filterPanel.repaint
+ }
+
+ val filterPanel = new BoxPanel(Orientation.Vertical) {}
+
+ private val mutatorBox = new ComboBox[Mutator[Key, Entry]](container.available)
+
+ private val addButton: Button = new Button{
+ action = Action("Add") {
+ addPanel(
+ new Mutator_Panel((true, Parameters.Colors.next,
+ mutatorBox.selection.item))
+ )
+ }
+ }
+
+ private val applyButton = new Button{
+ action = Action("Apply") {
+ container(getMutators(panels))
+ }
+ }
+
+ private val resetButton = new Button {
+ action = Action("Reset") {
+ panels = getPanels(container())
+ }
+ }
+
+ private val cancelButton = new Button{
+ action = Action("Close") {
+ close
+ }
+ }
+ defaultButton = cancelButton
+
+ private val botPanel = new BoxPanel(Orientation.Horizontal) {
+ border = new EmptyBorder(10, 0, 0, 0)
+
+ contents += mutatorBox
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += addButton
+
+ contents += Swing.HGlue
+ contents += Swing.RigidBox(new Dimension(30, 0))
+ contents += applyButton
+
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ contents += resetButton
+
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ contents += cancelButton
+ }
+
+ contents = new BorderPanel {
+ border = new EmptyBorder(5, 5, 5, 5)
+
+ add(new ScrollPane(filterPanel), BorderPanel.Position.Center)
+ add(botPanel, BorderPanel.Position.South)
+ }
+
+ private class Mutator_Panel(initials: Mutator_Markup)
+ extends BoxPanel(Orientation.Horizontal)
+ {
+ private val (_enabled, _color, _mutator) = initials
+
+ private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
+ var focusList = List[java.awt.Component]()
+ private val enabledBox = new iCheckBox("Enabled", _enabled)
+
+ border = new EmptyBorder(5, 5, 5, 5)
+ maximumSize = new Dimension(Integer.MAX_VALUE, 30)
+ background = _color
+
+ contents += new Label(_mutator.name) {
+ preferredSize = new Dimension(175, 20)
+ horizontalAlignment = Alignment.Left
+ if (_mutator.description != "") tooltip = _mutator.description
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += enabledBox
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ focusList = enabledBox.peer :: focusList
+ inputs.map( _ match {
+ case (n, c) => {
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ if (n != "") {
+ contents += new Label(n)
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ }
+ contents += c.asInstanceOf[Component]
+
+ focusList = c.asInstanceOf[Component].peer :: focusList
+ }
+ case _ =>
+ })
+
+ {
+ val t = this
+ contents += Swing.HGlue
+ contents += Swing.RigidBox(new Dimension(10, 0))
+
+ if (show_color_chooser) {
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Color") {
+ t.background =
+ JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ }
+
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Up") {
+ movePanelUp(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Down") {
+ movePanelDown(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Del") {
+ removePanel(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ }
+
+ focusList = focusList.reverse
+
+ private def isRegex(regex: String): Boolean = {
+ try {
+ regex.r
+
+ true
+ } catch {
+ case _: java.util.regex.PatternSyntaxException => false
+ }
+ }
+
+ def get_Mutator_Markup: Mutator_Markup = {
+ def regexOrElse(regex: String, orElse: String): String = {
+ if (isRegex(regex)) regex
+ else orElse
+ }
+
+ val m = _mutator match {
+ case Identity() =>
+ Identity()
+ case Node_Expression(r, _, _, _) =>
+ Node_Expression(
+ regexOrElse(inputs(2)._2.getString, r),
+ inputs(3)._2.getBool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.getBool,
+ inputs(0)._2.getBool
+ )
+ case Node_List(_, _, _, _) =>
+ Node_List(
+ inputs(2)._2.getString.split(',').filter(_ != "").toList,
+ inputs(3)._2.getBool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.getBool,
+ inputs(0)._2.getBool
+ )
+ case Edge_Endpoints(_, _) =>
+ Edge_Endpoints(
+ inputs(0)._2.getString,
+ inputs(1)._2.getString
+ )
+ case Edge_Transitive() =>
+ Edge_Transitive()
+ case Add_Node_Expression(r) =>
+ Add_Node_Expression(
+ regexOrElse(inputs(0)._2.getString, r)
+ )
+ case Add_Transitive_Closure(_, _) =>
+ Add_Transitive_Closure(
+ inputs(0)._2.getBool,
+ inputs(1)._2.getBool
+ )
+ case _ =>
+ Identity()
+ }
+
+ (enabledBox.selected, background, m)
+ }
+
+ private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match {
+ case Node_Expression(regex, reverse, check_parents, check_children) =>
+ List(
+ ("", new iCheckBox("Parents", check_children)),
+ ("", new iCheckBox("Children", check_parents)),
+ ("Regex", new iTextField(regex, x => !isRegex(x))),
+ ("", new iCheckBox(reverse_caption, reverse))
+ )
+ case Node_List(list, reverse, check_parents, check_children) =>
+ List(
+ ("", new iCheckBox("Parents", check_children)),
+ ("", new iCheckBox("Children", check_parents)),
+ ("Names", new iTextField(list.mkString(","))),
+ ("", new iCheckBox(reverse_caption, reverse))
+ )
+ case Edge_Endpoints(source, dest) =>
+ List(
+ ("Source", new iTextField(source)),
+ ("Destination", new iTextField(dest))
+ )
+ case Add_Node_Expression(regex) =>
+ List(
+ ("Regex", new iTextField(regex, x => !isRegex(x)))
+ )
+ case Add_Transitive_Closure(parents, children) =>
+ List(
+ ("", new iCheckBox("Parents", parents)),
+ ("", new iCheckBox("Children", children))
+ )
+ case _ => Nil
+ }
+ }
+
+ private trait Mutator_Input_Value
+ {
+ def getString: String
+ def getBool: Boolean
+ }
+
+ private class iTextField(t: String, colorator: String => Boolean)
+ extends TextField(t) with Mutator_Input_Value
+ {
+ def this(t: String) = this(t, x => false)
+
+ preferredSize = new Dimension(125, 18)
+
+ reactions += {
+ case ValueChanged(_) =>
+ if (colorator(text))
+ background = Color.RED
+ else
+ background = Color.WHITE
+ }
+
+ def getString = text
+ def getBool = true
+ }
+
+ private class iCheckBox(t: String, s: Boolean)
+ extends CheckBox(t) with Mutator_Input_Value
+ {
+ selected = s
+
+ def getString = ""
+ def getBool = selected
+ }
+
+ private object focusTraversal
+ extends FocusTraversalPolicy
+ {
+ private var items = Vector[java.awt.Component]()
+
+ def add(c: java.awt.Component) {
+ items = items :+ c
+ }
+ def addAll(cs: TraversableOnce[java.awt.Component]) {
+ items = items ++ cs
+ }
+ def clear() {
+ items = Vector[java.awt.Component]()
+ }
+
+ def getComponentAfter(root: java.awt.Container,
+ c: java.awt.Component): java.awt.Component = {
+ val i = items.indexOf(c)
+ if (i < 0) {
+ getDefaultComponent(root)
+ } else {
+ items((i + 1) % items.length)
+ }
+ }
+
+ def getComponentBefore(root: java.awt.Container,
+ c: java.awt.Component): java.awt.Component = {
+ val i = items.indexOf(c)
+ if (i < 0) {
+ getDefaultComponent(root)
+ } else {
+ items((i - 1) % items.length)
+ }
+ }
+
+ def getFirstComponent(root: java.awt.Container): java.awt.Component = {
+ if (items.length > 0)
+ items(0)
+ else
+ null
+ }
+
+ def getDefaultComponent(root: java.awt.Container)
+ : java.awt.Component = getFirstComponent(root)
+
+ def getLastComponent(root: java.awt.Container): java.awt.Component = {
+ if (items.length > 0)
+ items.last
+ else
+ null
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator_event.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,22 @@
+/* Title: Tools/Graphview/src/mutator_event.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Events for dialog synchronization.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.Color
+
+
+object Mutator_Event
+{
+ type Key = String
+ type Entry = Option[Locale]
+ type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
+
+ sealed abstract class Message
+ case class Add(m: Mutator_Markup) extends Message
+ case class NewList(m: List[Mutator_Markup]) extends Message
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/parameters.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,62 @@
+/* Title: Tools/Graphview/src/parameters.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Visual parameters with fallbacks for non-jEdit-environment.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.jedit._
+import java.awt.Color
+
+
+//LocaleBrowser may or may not run within jEdit, so all jEdit specific options
+//have to have fallbacks.
+object Parameters
+{
+ def font_family(): String =
+ try {
+ Isabelle.font_family()
+ }
+ catch { case _ => "IsabelleText" }
+
+ def font_size(): Int =
+ try {
+ scala.math.round(Isabelle.font_size())
+ }
+ catch { case _ => 16 }
+
+ //Should not fail since this is in the isabelle environment.
+ def tooltip_css(): String =
+ File.try_read(
+ Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS")))
+
+ object Colors {
+ 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 = {
+ this.synchronized {
+ curr = (curr + 1) % Filter_Colors.length
+ Filter_Colors(curr)
+ }
+ }
+
+ val Default = Color.WHITE
+ val No_Axioms = Color.LIGHT_GRAY
+ }
+
+ var long_names = true
+ var arrow_heads = false
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/popups.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,176 @@
+/* Title: Tools/Graphview/src/popups.scala
+ Author: Markus Kaiser, TU Muenchen
+
+PopupMenu generation for graph components.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+import javax.swing.JPopupMenu
+import scala.swing.{Action, Menu, MenuItem, Seperator}
+
+
+object Popups {
+ def apply(panel: Graph_Panel, under_mouse: Option[String],
+ selected: List[String]): JPopupMenu =
+ {
+ val add_mutator = panel.visualizer.model.Mutators.add _
+ val curr = panel.visualizer.model.current
+
+ def filter_context(ls: List[String], reverse: Boolean,
+ caption: String, edges: Boolean) =
+ new Menu(caption) {
+ contents += new MenuItem(new Action("This") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, false, false)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Family") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, true, true)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Parents") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, false, true)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Children") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, true, false)
+ )
+ )
+ })
+
+
+ if (edges) {
+ val outs = ls.map(l => (l, curr.imm_succs(l)))
+ .filter(_._2.size > 0).sortBy(_._1)
+ val ins = ls.map(l => (l, curr.imm_preds(l)))
+ .filter(_._2.size > 0).sortBy(_._1)
+
+ if (outs.nonEmpty || ins.nonEmpty) {
+ contents += new Separator()
+
+ contents += new Menu("Edge") {
+ if (outs.nonEmpty) {
+ contents += new MenuItem("From...") {
+ enabled = false
+ }
+
+ outs.map( e => {
+ val (from, tos) = e
+ contents += new Menu(from) {
+ contents += new MenuItem("To..."){
+ enabled = false
+ }
+
+ tos.toList.sorted.distinct.map( to => {
+ contents += new MenuItem(new Action(to) {
+ def apply =
+ add_mutator(
+ Mutators.create(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(Edge_Endpoints(from, to))
+ )
+ })
+ })
+ }
+ })
+ }
+ }
+ }
+ }
+ }
+
+ val popup = new JPopupMenu()
+
+ popup.add(new MenuItem(new Action("Remove all filters") {
+ def apply = panel.visualizer.model.Mutators(Nil)
+ }).peer
+ )
+ popup.add(new MenuItem(new Action("Remove transitive edges") {
+ def apply = add_mutator(Mutators.create(Edge_Transitive()))
+ }).peer
+ )
+ popup.add(new JPopupMenu.Separator)
+
+ if (under_mouse.isDefined) {
+ val v = under_mouse.get
+ popup.add(new MenuItem("Mouseover: %s".format(panel.visualizer.Caption(v))) {
+ enabled = false
+ }.peer)
+
+ popup.add(filter_context(List(v), true, "Hide", true).peer)
+ popup.add(filter_context(List(v), false, "Show only", false).peer)
+
+ popup.add(new JPopupMenu.Separator)
+ }
+ if (!selected.isEmpty) {
+ val text = {
+ if (selected.length > 1) {
+ "Multiple"
+ } else {
+ panel.visualizer.Caption(selected.head)
+ }
+ }
+
+ popup.add(new MenuItem("Selected: %s".format(text)) {
+ enabled = false
+ }.peer)
+
+ popup.add(filter_context(selected, true, "Hide", true).peer)
+ popup.add(filter_context(selected, false, "Show only", false).peer)
+ popup.add(new JPopupMenu.Separator)
+ }
+
+
+ popup.add(new MenuItem(new Action("Fit to Window") {
+ def apply = panel.fit_to_window()
+ }).peer
+ )
+
+ popup
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/shapes.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,250 @@
+/* Title: Tools/Graphview/src/shapes.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Drawable shapes.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.{BasicStroke, Graphics2D, Shape}
+import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D}
+
+
+object Shapes {
+ trait Node {
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]): Shape
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]): Unit
+ }
+
+ object Growing_Node extends Node {
+ private val stroke =
+ new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]) = {
+ val caption = vis.Caption(peer.get)
+ val bounds = g.getFontMetrics.getStringBounds(caption, g)
+ val (x, y) = vis.Coordinates(peer.get)
+
+ new Rectangle2D.Double(
+ x -(bounds.getWidth / 2 + 25),
+ y -(bounds.getHeight / 2 + 5),
+ bounds.getWidth + 50,
+ bounds.getHeight + 10
+ )
+ }
+
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]) {
+ val caption = vis.Caption(peer.get)
+ val bounds = g.getFontMetrics.getStringBounds(caption, g)
+ val s = shape(g, vis, peer)
+
+ val (border, background, foreground) = vis.Color(peer)
+ g.setStroke(stroke)
+ g.setColor(border)
+ g.draw(s)
+ g.setColor(background)
+ g.fill(s)
+ g.setColor(foreground)
+ g.drawString(caption,
+ (s.getCenterX + (-bounds.getWidth / 2)).toFloat,
+ (s.getCenterY + 5).toFloat
+ )
+ }
+ }
+
+ object Dummy extends Node {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+ private val shape = new Rectangle2D.Double(-8, -8, 16, 16)
+ private val identity = new AffineTransform()
+
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]) = shape
+
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]) =
+ paint_transformed(g, vis, peer, identity)
+
+ def paint_transformed(g: Graphics2D, vis: Visualizer,
+ peer: Option[String], at: AffineTransform) = {
+ val (border, background, foreground) = vis.Color(peer)
+ g.setStroke(stroke)
+ g.setColor(border)
+ g.draw(at.createTransformedShape(shape))
+ }
+ }
+
+ trait Edge {
+ def paint(g: Graphics2D, vis: Visualizer, peer: (String, String),
+ head: Boolean, dummies: Boolean)
+ }
+
+ object Straight_Edge extends Edge {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+ def paint(g: Graphics2D, vis: Visualizer,
+ peer: (String, String), head: Boolean, dummies: Boolean) {
+ val ((fx, fy), (tx, ty)) =
+ (vis.Coordinates(peer._1), vis.Coordinates(peer._2))
+ val ds = {
+ val (min, max) = (math.min(fy, ty), math.max(fy, ty))
+
+ vis.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+ }
+ val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+
+ path.moveTo(fx, fy)
+ ds.foreach({case (x, y) => path.lineTo(x, y)})
+ path.lineTo(tx, ty)
+
+ if (dummies) {
+ ds.foreach({
+ case (x, y) => {
+ val at = AffineTransform.getTranslateInstance(x, y)
+ Dummy.paint_transformed(g, vis, None, at)
+ }
+ })
+ }
+
+ g.setStroke(stroke)
+ g.setColor(vis.Color(peer))
+ g.draw(path)
+
+ if (head) Arrow_Head.paint(g, path, vis.Drawer.shape(g, Some(peer._2)))
+ }
+ }
+
+ object Cardinal_Spline_Edge extends Edge {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+ private val slack = 0.1
+
+ def paint(g: Graphics2D, vis: Visualizer,
+ peer: (String, String), head: Boolean, dummies: Boolean) {
+ val ((fx, fy), (tx, ty)) =
+ (vis.Coordinates(peer._1), vis.Coordinates(peer._2))
+ val ds = {
+ val (min, max) = (math.min(fy, ty), math.max(fy, ty))
+
+ vis.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+ }
+
+ if (ds.isEmpty) Straight_Edge.paint(g, vis, peer, head, dummies)
+ else {
+ val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+ path.moveTo(fx, fy)
+
+ val coords = ((fx, fy) :: ds ::: List((tx, ty)))
+ val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+
+ val (dx2, dy2) =
+ ((dx, dy) /: coords.sliding(3))({
+ case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
+ val (dx2, dy2) = (rx - lx, ry - ly)
+
+ path.curveTo(lx + slack * dx , ly + slack * dy,
+ mx - slack * dx2, my - slack * dy2,
+ mx , my)
+ (dx2, dy2)
+ }
+ })
+
+ val (lx, ly) = ds.last
+ path.curveTo(lx + slack * dx2, ly + slack * dy2,
+ tx - slack * dx2, ty - slack * dy2,
+ tx , ty)
+
+ if (dummies) {
+ ds.foreach({
+ case (x, y) => {
+ val at = AffineTransform.getTranslateInstance(x, y)
+ Dummy.paint_transformed(g, vis, None, at)
+ }
+ })
+ }
+
+ g.setStroke(stroke)
+ g.setColor(vis.Color(peer))
+ g.draw(path)
+
+ if (head) Arrow_Head.paint(g, path, vis.Drawer.shape(g, Some(peer._2)))
+ }
+ }
+ }
+
+ object Arrow_Head {
+ type Point = (Double, Double)
+
+ private def position(path: GeneralPath,
+ shape: Shape): Option[AffineTransform] = {
+ def intersecting_line(path: GeneralPath,
+ shape: Shape): Option[(Point, Point)] = {
+ import java.awt.geom.PathIterator
+
+ val i = path.getPathIterator(null, 1d)
+ var seg = Array[Double](0,0,0,0,0,0)
+ var p1 = (0d, 0d)
+ var p2 = (0d, 0d)
+ while (!i.isDone()) {
+ i.currentSegment(seg) match {
+ case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
+ case PathIterator.SEG_LINETO => {
+ p1 = p2
+ p2 = (seg(0), seg(1))
+
+ if(shape.contains(seg(0), seg(1)))
+ return Some((p1, p2))
+ }
+ case _ =>
+ }
+ i.next()
+ }
+
+ None
+ }
+
+ def binary_search(line: (Point, Point),
+ shape: Shape): Option[AffineTransform] = {
+ val ((fx, fy), (tx, ty)) = line
+ if (shape.contains(fx, fy) == shape.contains(tx, ty))
+ None
+ else {
+ val (dx, dy) = (fx - tx, fy - ty)
+ if ( (dx * dx + dy * dy) < 1d ) {
+ val at = AffineTransform.getTranslateInstance(fx, fy)
+ at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
+ Some(at)
+ } else {
+ val (mx, my) = (fx + (tx - fx) / 2d, fy + (ty - fy) / 2d)
+ if (shape.contains(fx, fy) == shape.contains(mx, my))
+ binary_search(((mx, my), (tx, ty)), shape)
+ else
+ binary_search(((fx, fy), (mx, my)), shape)
+ }
+ }
+ }
+
+ intersecting_line(path, shape) match {
+ case None => None
+ case Some(line) => binary_search(line, shape)
+ }
+ }
+
+ def paint(g: Graphics2D, path: GeneralPath, shape: Shape) {
+ position(path, shape) match {
+ case None =>
+ case Some(at) => {
+ val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
+ arrow.moveTo(0, 0)
+ arrow.lineTo(-20, 8)
+ arrow.lineTo(-13, 0)
+ arrow.lineTo(-20, -8)
+ arrow.lineTo(0, 0)
+ arrow.transform(at)
+
+ g.fill(arrow)
+ }
+ }
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/tooltips.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,93 @@
+/* Title: Tools/Graphview/src/graph_components.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Tooltip generation for graph components.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import java.awt.FontMetrics
+
+
+object Tooltips {
+ // taken (and modified slightly) from html_panel.scala
+ private def make_HTML(term: XML.Body, fm: FontMetrics): String = {
+ XML.string_of_body ( term.flatMap(div =>
+ Pretty.formatted(List(div), 76, Pretty.font_metric(fm))
+ .map( t=>
+ HTML.spans(t, false))
+ ).head
+ )
+ }
+
+ def locale(key: String, model: Model, fm: FontMetrics): String = {
+ val locale = model.complete.get_node(key)
+ val parsed_name = key.split('.')
+
+ if (!locale.isDefined) {
+ """|<html>
+ |<body style="margin: 3px">
+ |%s
+ |</body>
+ |""".stripMargin.format(parsed_name.reduceLeft("%s<br>%s".format(_,_)))
+ } else {
+ val Some(Locale(axioms, parameters)) = locale
+
+ val parms = {
+ if (parameters.size > 0) {
+ """|
+ |<p>Parameters:</p>
+ |<ul>
+ |%s
+ |</ul>
+ |""".stripMargin.format(parameters.map(
+ y => "<li>%s :: %s</li>".format(
+ y._1,
+ make_HTML(y._2, fm))
+ ).reduceLeft(_+_))
+ } else ""
+ }
+ val axms = {
+ if (axioms.size > 0) {
+ """|
+ |<p>Axioms:</p>
+ |<ul>
+ |%s
+ |</ul>
+ |""".stripMargin.format(axioms.map(
+ y => "<li>%s</li>".format(
+ make_HTML(y, fm))
+ ).reduceLeft(_+_))
+ } else ""
+ }
+
+ """|<html>
+ |<style type="text/css">
+ |/* isabelle style */
+ |%s
+ |
+ |/* tooltip specific style */
+ |
+ |body { margin: 10px; font-size: 12px; }
+ |hr { margin: 12px 0 0 0; height: 2px; }
+ |p { margin: 6px 0 2px 0; }
+ |ul { margin: 0 0 0 4px; list-style-type: none; }
+ |li { margin: 0 0 4px; }
+ |
+ |</style>
+ |<body>
+ |<center>%s</center>
+ |<hr>
+ |%s
+ |%s
+ |</body>
+ |</html>
+ |""".stripMargin.format(Parameters.tooltip_css,
+ parsed_name.reduceLeft("%s<br>%s".format(_,_)),
+ axms,
+ parms).replace("'", "'")
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/visualizer.scala Mon Sep 24 20:22:58 2012 +0200
@@ -0,0 +1,160 @@
+/* Title: Tools/Graphview/src/visualizer.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graph visualization interface.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.{RenderingHints, Graphics2D}
+
+
+class Visualizer(val model: Model) {
+ object Coordinates {
+ private var nodes = Map[String, (Double, Double)]()
+ private var dummies = Map[(String, String), List[(Double, Double)]]()
+
+ def apply(k: String): (Double, Double) = nodes.get(k) match {
+ case Some(c) => c
+ case None => (0, 0)
+ }
+
+ def apply(e: (String, String)): List[(Double, Double)] = dummies.get(e) match {
+ case Some(ds) => ds
+ case None => Nil
+ }
+
+ def translate(k: String, by: (Double, Double)) {
+ val ((x, y), (dx, dy)) = (Coordinates(k), by)
+ reposition(k, (x + dx, y + dy))
+ }
+
+ def reposition(k: String, to: (Double, Double)) {
+ nodes += (k -> to)
+ }
+
+ def translate(d: ((String, String), Int), by: (Double, Double)) {
+ val ((e, i),(dx, dy)) = (d, by)
+ val (x, y) = apply(e)(i)
+ reposition(d, (x + dx, y + dy))
+ }
+
+ def reposition(d: ((String, String), Int), to: (Double, Double)) {
+ val (e, index) = d
+ dummies.get(e) match {
+ case None =>
+ case Some(ds) =>
+ dummies += ( e ->
+ (ds.zipWithIndex :\ List[(Double, Double)]()){
+ case ((t, i), n) => if (index == i) to :: n
+ else t :: n
+ }
+ )
+ }
+ }
+
+ def layout() {
+ val (l, d) = Layout_Pendulum(model.current)
+ nodes = l
+ dummies = d
+ }
+
+ def bounds(): (Double, Double, Double, Double) =
+ model.visible_nodes().toList match {
+ case Nil => (0, 0, 0, 0)
+ case nodes => {
+ val X: (String => Double) = {n => apply(n)._1}
+ val Y: (String => Double) = {n => apply(n)._2}
+
+ (X(nodes.minBy(X)), Y(nodes.minBy(Y)),
+ X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
+ }
+ }
+ }
+
+ private val visualizer = this
+ object Drawer {
+ import Shapes._
+ import java.awt.Shape
+
+ def apply(g: Graphics2D, n: Option[String]) = n match {
+ case None =>
+ case Some(_) => Growing_Node.paint(g, visualizer, n)
+ }
+
+ def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) = {
+ Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
+ }
+
+ def paint_all_visible(g: Graphics2D, dummies: Boolean) = {
+ g.setFont(Font())
+ g.setRenderingHints(rendering_hints)
+
+ model.visible_edges().foreach(e => {
+ apply(g, e, Parameters.arrow_heads, dummies)
+ })
+
+ model.visible_nodes().foreach(l => {
+ apply(g, Some(l))
+ })
+ }
+
+ def shape(g: Graphics2D, n: Option[String]): Shape = n match {
+ case None => Dummy.shape(g, visualizer, None)
+ case Some(_) => Growing_Node.shape(g, visualizer, n)
+ }
+ }
+
+ object Selection {
+ private var selected: List[String] = Nil
+
+ def apply() = selected
+ def apply(s: String) = selected.contains(s)
+
+ def add(s: String) { selected = s :: selected }
+ def set(ss: List[String]) { selected = ss }
+ def clear() { selected = Nil }
+ }
+
+ object Color {
+ import java.awt.{Color => awtColor}
+
+ def apply(l: Option[String]): (awtColor, awtColor, awtColor) = l match {
+ case None => (awtColor.GRAY, awtColor.WHITE, awtColor.BLACK)
+ case Some(c) => {
+ if (Selection(c))
+ (awtColor.BLUE, awtColor.GREEN, awtColor.BLACK)
+ else
+ (awtColor.BLACK,
+ model.colors.getOrElse(c, awtColor.WHITE), awtColor.BLACK)
+ }
+ }
+
+ def apply(e: (String, String)): awtColor = awtColor.BLACK
+ }
+
+ object Caption {
+ def apply(k: String) =
+ if (Parameters.long_names) k
+ else k.split('.').last
+ }
+
+ object Tooltip {
+ import java.awt.FontMetrics
+
+ def apply(l: String, fm: FontMetrics) = Tooltips.locale(l, model, fm)
+ }
+
+ object Font {
+ import java.awt.{Font => awtFont}
+
+ def apply() = new awtFont(Parameters.font_family,
+ awtFont.BOLD, Parameters.font_size)
+ }
+
+ val rendering_hints =
+ new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON)
+}
\ No newline at end of file