src/Tools/Graphview/layout.scala
author wenzelm
Tue, 06 Jan 2015 16:43:17 +0100
changeset 59304 848e27e4ac37
parent 59302 4d985afc0565
child 59305 b5e33012180e
permissions -rw-r--r--
proper translate vertex (cf. 4d985afc0565);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59232
07a7dfd6d694 tuned signature;
wenzelm
parents: 59202
diff changeset
     1
/*  Title:      Tools/Graphview/layout.scala
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     2
    Author:     Markus Kaiser, TU Muenchen
59240
e411afcfaa29 tuned headers;
wenzelm
parents: 59232
diff changeset
     3
    Author:     Makarius
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     4
59261
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
     5
DAG layout algorithm, according to:
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
     6
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
     7
  Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
     8
  DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
     9
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
    10
  http://dx.doi.org/10.1007/3-540-58950-3_371
5e7280814916 tuned comments;
wenzelm
parents: 59260
diff changeset
    11
  ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    12
*/
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    13
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    14
package isabelle.graphview
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    15
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    16
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    17
import isabelle._
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    18
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    19
59232
07a7dfd6d694 tuned signature;
wenzelm
parents: 59202
diff changeset
    20
object Layout
49744
84904ce4905b tuned source structure;
wenzelm
parents: 49737
diff changeset
    21
{
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    22
  /* graph structure */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    23
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    24
  object Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    25
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    26
    object Ordering extends scala.math.Ordering[Vertex]
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    27
    {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    28
      def compare(v1: Vertex, v2: Vertex): Int =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    29
        (v1, v2) match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    30
          case (_: Node, _: Dummy) => -1
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    31
          case (_: Dummy, _: Node) => 1
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    32
          case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    33
          case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    34
            Graph_Display.Node.Ordering.compare(a1, b1) match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    35
              case 0 =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    36
                Graph_Display.Node.Ordering.compare(a2, b2) match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    37
                  case 0 => i compare j
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    38
                  case ord => ord
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    39
                }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    40
              case ord => ord
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    41
            }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    42
        }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    43
    }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    44
  }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    45
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    46
  sealed abstract class Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    47
  case class Node(node: Graph_Display.Node) extends Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    48
  case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    49
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
    50
  object Point { val zero: Point = Point(0.0, 0.0) }
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
    51
  case class Point(x: Double, y: Double)
50469
wenzelm
parents: 50468
diff changeset
    52
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    53
  type Graph = isabelle.Graph[Vertex, Point]
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    54
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    55
  def make_graph(entries: List[((Vertex, Point), List[Vertex])]): Graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    56
    isabelle.Graph.make(entries)(Vertex.Ordering)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
    57
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    58
  val empty_graph: Graph = make_graph(Nil)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    59
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    60
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    61
  /* layout */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    62
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    63
  val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
50470
wenzelm
parents: 50469
diff changeset
    64
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    65
  val pendulum_iterations = 10
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
    66
  val minimize_crossings_iterations = 40
50469
wenzelm
parents: 50468
diff changeset
    67
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    68
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    69
  private type Levels = Map[Vertex, Int]
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    70
  private val empty_levels: Levels = Map.empty
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    71
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    72
  def make(metrics: Metrics, input_graph: Graph_Display.Graph): Layout =
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
    73
  {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    74
    if (input_graph.is_empty) empty
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    75
    else {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    76
      /* initial graph */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    77
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    78
      val initial_graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    79
        make_graph(
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    80
          input_graph.iterator.map(
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    81
            { case (a, (_, (_, bs))) => ((Node(a), Point.zero), bs.toList.map(Node(_))) }).toList)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    82
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    83
      val initial_levels: Levels =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    84
        (empty_levels /: initial_graph.topological_order) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    85
          case (levels, vertex) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    86
            val level =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    87
              1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    88
            levels + (vertex -> level)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    89
        }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    90
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    91
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    92
      /* graph with dummies */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    93
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    94
      val (dummy_graph, dummy_levels) =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    95
        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    96
            case ((graph, levels), (node1, node2)) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    97
              val v1 = Node(node1); val l1 = levels(v1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    98
              val v2 = Node(node2); val l2 = levels(v2)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    99
              if (l2 - l1 <= 1) (graph, levels)
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   100
              else {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   101
                val dummies_levels =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   102
                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   103
                    yield (Dummy(node1, node2, i), l)).toList
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   104
                val dummies = dummies_levels.map(_._1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   105
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   106
                val levels1 = (levels /: dummies_levels)(_ + _)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   107
                val graph1 =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   108
                  ((graph /: dummies)(_.new_node(_, Point.zero)).del_edge(v1, v2) /:
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   109
                    (v1 :: dummies ::: List(v2)).sliding(2)) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   110
                      case (g, List(a, b)) => g.add_edge(a, b) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   111
                (graph1, levels1)
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   112
              }
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   113
          }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   114
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   115
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   116
      /* minimize edge crossings and initial coordinates */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   117
50469
wenzelm
parents: 50468
diff changeset
   118
      val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
wenzelm
parents: 50468
diff changeset
   119
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   120
      val levels_graph: Graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   121
        (((dummy_graph, 0.0) /: levels) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   122
          case ((graph, y), level) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   123
            ((((graph, 0.0) /: level) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   124
              case ((g, x), v) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   125
                val w2 = metrics.box_width2(v)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   126
                (g.map_node(v, _ => Point(x + w2, y)), x + 2 * w2 + metrics.box_gap)
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   127
            })._1, y + metrics.box_height(level.length))
50474
6ee044e2d1a7 initial layout coordinates more like old browser;
wenzelm
parents: 50470
diff changeset
   128
        })._1
6ee044e2d1a7 initial layout coordinates more like old browser;
wenzelm
parents: 50470
diff changeset
   129
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   130
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   131
      /* pendulum layout */
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   132
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   133
      val output_graph = pendulum(metrics, levels_graph, levels)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   134
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   135
      new Layout(metrics, input_graph, output_graph)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   136
    }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   137
  }
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
   138
49744
84904ce4905b tuned source structure;
wenzelm
parents: 49737
diff changeset
   139
84904ce4905b tuned source structure;
wenzelm
parents: 49737
diff changeset
   140
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   141
  /** edge crossings **/
50469
wenzelm
parents: 50468
diff changeset
   142
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   143
  private type Level = List[Vertex]
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
   144
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   145
  def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
49745
083accbfa77d more conventional Double constants;
wenzelm
parents: 49744
diff changeset
   146
  {
50469
wenzelm
parents: 50468
diff changeset
   147
    def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   148
      child.map(v => {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   149
          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
50469
wenzelm
parents: 50468
diff changeset
   150
          val weight =
50468
7a2a4b84c5ee tuned min/max;
wenzelm
parents: 50467
diff changeset
   151
            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   152
          (v, weight)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   153
      }).sortBy(_._2).map(_._1)
50469
wenzelm
parents: 50468
diff changeset
   154
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   155
    def resort(levels: List[Level], top_down: Boolean) =
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   156
      if (top_down)
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   157
        (List(levels.head) /: levels.tail)((tops, bot) =>
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   158
          resort_level(tops.head, bot, top_down) :: tops).reverse
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   159
      else {
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   160
        val rev_levels = levels.reverse
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   161
        (List(rev_levels.head) /: rev_levels.tail)((bots, top) =>
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   162
          resort_level(bots.head, top, top_down) :: bots)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   163
      }
50469
wenzelm
parents: 50468
diff changeset
   164
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
   165
    ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   166
      case ((old_levels, old_crossings, top_down), _) => {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   167
          val new_levels = resort(old_levels, top_down)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   168
          val new_crossings = count_crossings(graph, new_levels)
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
   169
          if (new_crossings < old_crossings)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   170
            (new_levels, new_crossings, !top_down)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   171
          else
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   172
            (old_levels, old_crossings, !top_down)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   173
      }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   174
    }._1
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   175
  }
50469
wenzelm
parents: 50468
diff changeset
   176
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   177
  def level_list(levels: Levels): List[Level] =
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   178
  {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   179
    val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   180
    val buckets = new Array[Level](max_lev + 1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   181
    for (l <- 0 to max_lev) { buckets(l) = Nil }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   182
    for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   183
    buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   184
  }
50469
wenzelm
parents: 50468
diff changeset
   185
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   186
  def count_crossings(graph: Graph, levels: List[Level]): Int =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   187
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   188
    def in_level(ls: List[Level]): Int = ls match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   189
      case List(top, bot) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   190
        top.iterator.zipWithIndex.map {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   191
          case (outer_parent, outer_parent_index) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   192
            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   193
            .map(outer_child =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   194
              (0 until outer_parent_index)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   195
              .map(inner_parent =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   196
                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   197
                .filter(inner_child => outer_child < inner_child)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   198
                .size
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   199
              ).sum
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   200
            ).sum
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   201
        }.sum
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   202
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   203
      case _ => 0
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   204
    }
50469
wenzelm
parents: 50468
diff changeset
   205
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   206
    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   207
  }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   208
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   209
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   210
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   211
  /** pendulum method **/
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   212
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   213
  /*This is an auxiliary class which is used by the layout algorithm when
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   214
    calculating coordinates with the "pendulum method". A "region" is a
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   215
    group of vertices which "stick together".*/
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   216
  private class Region(init: Vertex)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   217
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   218
    var content: List[Vertex] = List(init)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   219
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   220
    def distance(metrics: Metrics, graph: Graph, that: Region): Double =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   221
    {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   222
      val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   223
      val v2 = that.content.head; val x2 = graph.get_node(v2).x - metrics.box_width2(v2)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   224
      x2 - x1 - metrics.box_gap
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   225
    }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   226
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   227
    def deflection(graph: Graph, top_down: Boolean): Double =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   228
      ((for (a <- content.iterator) yield {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   229
        val x = graph.get_node(a).x
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   230
        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   231
        bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   232
      }).sum / content.length).round.toDouble
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   233
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   234
    def move(graph: Graph, dx: Double): Graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   235
      if (dx == 0.0) graph
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   236
      else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   237
  }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   238
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   239
  private type Regions = List[List[Region]]
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   240
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   241
  def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   242
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   243
    def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   244
    {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   245
      val (graph1, regions1, moved) =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   246
      ((graph, List.empty[List[Region]], false) /: (if (top_down) regions else regions.reverse)) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   247
        case ((graph, tops, moved), bot) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   248
          val bot1 = collapse(graph, bot, top_down)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   249
          val (graph1, moved1) = deflect(graph, bot1, top_down)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   250
          (graph1, bot1 :: tops, moved || moved1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   251
      }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   252
      (graph1, regions1.reverse, moved)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   253
    }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   254
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   255
    def collapse(graph: Graph, level: List[Region], top_down: Boolean): List[Region] =
50469
wenzelm
parents: 50468
diff changeset
   256
    {
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   257
      if (level.size <= 1) level
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   258
      else {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   259
        var next = level
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   260
        var regions_changed = true
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   261
        while (regions_changed) {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   262
          regions_changed = false
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   263
          for (i <- Range(next.length - 1, 0, -1)) {
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   264
            val (r1, r2) = (next(i - 1), next(i))
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   265
            val d1 = r1.deflection(graph, top_down)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   266
            val d2 = r2.deflection(graph, top_down)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   267
50469
wenzelm
parents: 50468
diff changeset
   268
            if (// Do regions touch?
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   269
                r1.distance(metrics, graph, r2) <= 0.0 &&
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   270
                // Do they influence each other?
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   271
                (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   272
            {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   273
              regions_changed = true
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   274
              r1.content = r1.content ::: r2.content
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   275
              next = next.filter(next.indexOf(_) != i)
50469
wenzelm
parents: 50468
diff changeset
   276
            }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   277
          }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   278
        }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   279
        next
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   280
      }
50469
wenzelm
parents: 50468
diff changeset
   281
    }
wenzelm
parents: 50468
diff changeset
   282
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   283
    def deflect(graph: Graph, level: List[Region], top_down: Boolean): (Graph, Boolean) =
50469
wenzelm
parents: 50468
diff changeset
   284
    {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   285
      ((graph, false) /: (0 until level.length)) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   286
        case ((graph, moved), i) =>
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   287
          val r = level(i)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   288
          val d = r.deflection(graph, top_down)
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   289
          val offset =
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   290
            if (d < 0 && i > 0)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   291
              - (level(i - 1).distance(metrics, graph, r) min (- d))
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   292
            else if (d >= 0 && i < level.length - 1)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   293
              r.distance(metrics, graph, level(i + 1)) min d
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   294
            else d
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   295
          (r.move(graph, offset), moved || d != 0)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   296
      }
50469
wenzelm
parents: 50468
diff changeset
   297
    }
wenzelm
parents: 50468
diff changeset
   298
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   299
    val initial_regions = levels.map(level => level.map(new Region(_)))
50469
wenzelm
parents: 50468
diff changeset
   300
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   301
    ((levels_graph, initial_regions, true, true) /: (1 to pendulum_iterations)) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   302
      case ((graph, regions, top_down, moved), _) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   303
        if (moved) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   304
          val (graph1, regions1, moved1) = iteration(graph, regions, top_down)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   305
          (graph1, regions1, !top_down, moved1)
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   306
        }
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   307
        else (graph, regions, !top_down, moved)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   308
    }._1
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   309
  }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   310
}
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   311
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   312
final class Layout private(
59290
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   313
  val metrics: Metrics,
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   314
  val input_graph: Graph_Display.Graph,
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   315
  val output_graph: Layout.Graph)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   316
{
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   317
  /* vertex coordinates */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   318
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   319
  def get_vertex(v: Layout.Vertex): Layout.Point =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   320
    if (output_graph.defined(v)) output_graph.get_node(v)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   321
    else Layout.Point.zero
59290
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   322
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   323
  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   324
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   325
    if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   326
    else {
59304
848e27e4ac37 proper translate vertex (cf. 4d985afc0565);
wenzelm
parents: 59302
diff changeset
   327
      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dx, p.y + dy))
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   328
      new Layout(metrics, input_graph, output_graph1)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   329
    }
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   330
  }
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   331
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   332
59290
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   333
  /* dummies */
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   334
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   335
  def find_dummy(pred: Layout.Point => Boolean): Option[Layout.Dummy] =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   336
    output_graph.iterator.collectFirst({ case (d: Layout.Dummy, (p, _)) if pred(p) => d })
59292
fef652c88263 proper bounding box including dummies;
wenzelm
parents: 59290
diff changeset
   337
fef652c88263 proper bounding box including dummies;
wenzelm
parents: 59290
diff changeset
   338
  def dummies_iterator: Iterator[Layout.Point] =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   339
    for ((_: Layout.Dummy, (p, _)) <- output_graph.iterator) yield p
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   340
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   341
  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Point] =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   342
    new Iterator[Layout.Point] {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   343
      private var index = 0
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   344
      def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   345
      def next: Layout.Point =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   346
      {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   347
        val p = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   348
        index += 1
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   349
        p
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   350
      }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   351
    }
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   352
}
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   353