src/Tools/Graphview/layout.scala
author wenzelm
Mon, 01 Mar 2021 22:26:33 +0100
changeset 73591 2dd1fd9112d9
parent 73587 0af9e7e4476f
child 73606 d8a0e996614b
permissions -rw-r--r--
tuned --- silence odd warning;
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
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
     5
DAG layout according to:
59261
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
67601
b34be3010273 use preferred resolver according to DOI Handbook ยง3.8
Lars Hupel <lars.hupel@mytum.de>
parents: 59447
diff changeset
    10
  https://doi.org/10.1007/3-540-58950-3_371
59261
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(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    31
          case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    32
            Graph_Display.Node.Ordering.compare(a1, b1) match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    33
              case 0 =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    34
                Graph_Display.Node.Ordering.compare(a2, b2) match {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    35
                  case 0 => i compare j
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    36
                  case ord => ord
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    37
                }
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
            }
59311
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    40
          case (Node(a), Dummy(b, _, _)) =>
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    41
            Graph_Display.Node.Ordering.compare(a, b) match {
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    42
              case 0 => -1
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    43
              case ord => ord
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    44
            }
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    45
          case (Dummy(a, _, _), Node(b)) =>
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    46
            Graph_Display.Node.Ordering.compare(a, b) match {
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    47
              case 0 => 1
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    48
              case ord => ord
a269cc01e8eb clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
wenzelm
parents: 59310
diff changeset
    49
            }
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    50
        }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    51
    }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    52
  }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    53
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    54
  sealed abstract class Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    55
  case class Node(node: Graph_Display.Node) extends Vertex
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    56
  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
    57
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    58
  sealed case class Info(
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    59
    x: Double, y: Double, width2: Double, height2: Double, lines: List[String])
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    60
  {
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    61
    def left: Double = x - width2
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    62
    def right: Double = x + width2
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    63
    def width: Double = 2 * width2
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    64
    def height: Double = 2 * height2
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    65
  }
50469
wenzelm
parents: 50468
diff changeset
    66
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    67
  type Graph = isabelle.Graph[Vertex, Info]
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    68
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    69
  def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    70
    isabelle.Graph.make(entries)(Vertex.Ordering)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
    71
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    72
  val empty_graph: Graph = make_graph(Nil)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    73
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    74
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    75
  /* vertex x coordinate */
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    76
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    77
  private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    78
  private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    79
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    80
  private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    81
    if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx))
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    82
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
    83
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    84
  /* layout */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    85
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    86
  val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
50470
wenzelm
parents: 50469
diff changeset
    87
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    88
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    89
  private type Levels = Map[Vertex, Int]
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    90
  private val empty_levels: Levels = Map.empty
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    91
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    92
  def make(options: Options, metrics: Metrics,
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    93
    node_text: (Graph_Display.Node, XML.Body) => String,
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
    94
    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
    95
  {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    96
    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
    97
    else {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    98
      /* initial graph */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
    99
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   100
      val initial_graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   101
        make_graph(
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   102
          input_graph.iterator.map(
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   103
            { case (a, (content, (_, bs))) =>
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   104
                val lines = split_lines(node_text(a, content))
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   105
                val w2 = metrics.node_width2(lines)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   106
                val h2 = metrics.node_height2(lines.length)
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71592
diff changeset
   107
                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   108
            }).toList)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   109
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   110
      val initial_levels: Levels =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   111
        (empty_levels /: initial_graph.topological_order) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   112
          case (levels, vertex) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   113
            val level =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   114
              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
   115
            levels + (vertex -> level)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   116
        }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   117
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   118
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   119
      /* graph with dummies */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   120
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   121
      val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   122
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   123
      val (dummy_graph, dummy_levels) =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   124
        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   125
            case ((graph, levels), (node1, node2)) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   126
              val v1 = Node(node1); val l1 = levels(v1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   127
              val v2 = Node(node2); val l2 = levels(v2)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   128
              if (l2 - l1 <= 1) (graph, levels)
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   129
              else {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   130
                val dummies_levels =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   131
                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   132
                    yield (Dummy(node1, node2, i), l)).toList
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   133
                val dummies = dummies_levels.map(_._1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   134
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   135
                val levels1 = (levels /: dummies_levels)(_ + _)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   136
                val graph1 =
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   137
                  ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   138
                    (v1 :: dummies ::: List(v2)).sliding(2)) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   139
                      case (g, List(a, b)) => g.add_edge(a, b) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   140
                (graph1, levels1)
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   141
              }
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   142
          }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   143
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   144
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   145
      /* minimize edge crossings and initial coordinates */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   146
59313
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   147
      val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
50469
wenzelm
parents: 50468
diff changeset
   148
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   149
      val levels_graph: Graph =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   150
        (((dummy_graph, 0.0) /: levels) {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   151
          case ((graph, y), level) =>
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   152
            val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
59312
c4b9b04bfc6d proper level distance according to number of edges, as in old browser;
wenzelm
parents: 59311
diff changeset
   153
            val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   154
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   155
            val y1 = y + metrics.node_height2(num_lines)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   156
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   157
            val graph1 =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   158
              (((graph, 0.0) /: level) { case ((g, x), v) =>
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   159
                val info = g.get_node(v)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   160
                val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   161
                val x1 = x + info.width + metrics.gap
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   162
                (g1, x1)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   163
              })._1
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   164
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   165
            val y2 = y1 + metrics.level_height2(num_lines, num_edges)
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   166
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   167
            (graph1, y2)
50474
6ee044e2d1a7 initial layout coordinates more like old browser;
wenzelm
parents: 50470
diff changeset
   168
        })._1
6ee044e2d1a7 initial layout coordinates more like old browser;
wenzelm
parents: 50470
diff changeset
   169
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   170
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   171
      /* pendulum/rubberband layout */
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   172
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   173
      val output_graph =
59313
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   174
        rubberband(options, metrics, levels,
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   175
          pendulum(options, metrics, levels, levels_graph))
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   176
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   177
      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
   178
    }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   179
  }
49737
dd6fc7c9504a avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents: 49565
diff changeset
   180
49744
84904ce4905b tuned source structure;
wenzelm
parents: 49737
diff changeset
   181
84904ce4905b tuned source structure;
wenzelm
parents: 49737
diff changeset
   182
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   183
  /** edge crossings **/
50469
wenzelm
parents: 50468
diff changeset
   184
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   185
  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
   186
59313
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   187
  private def minimize_crossings(
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   188
    options: Options, graph: Graph, levels: List[Level]): List[Level] =
49745
083accbfa77d more conventional Double constants;
wenzelm
parents: 49744
diff changeset
   189
  {
59306
wenzelm
parents: 59305
diff changeset
   190
    def resort(parent: Level, child: Level, top_down: Boolean): Level =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   191
      child.map(v => {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   192
          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
50469
wenzelm
parents: 50468
diff changeset
   193
          val weight =
50468
7a2a4b84c5ee tuned min/max;
wenzelm
parents: 50467
diff changeset
   194
            (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
   195
          (v, weight)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   196
      }).sortBy(_._2).map(_._1)
50469
wenzelm
parents: 50468
diff changeset
   197
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   198
    ((levels, count_crossings(graph, levels)) /:
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   199
      (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   200
      case ((old_levels, old_crossings), iteration) =>
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   201
        val top_down = (iteration % 2 == 1)
59306
wenzelm
parents: 59305
diff changeset
   202
        val new_levels =
wenzelm
parents: 59305
diff changeset
   203
          if (top_down)
wenzelm
parents: 59305
diff changeset
   204
            (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
wenzelm
parents: 59305
diff changeset
   205
              resort(tops.head, bot, top_down) :: tops).reverse
wenzelm
parents: 59305
diff changeset
   206
          else {
wenzelm
parents: 59305
diff changeset
   207
            val rev_old_levels = old_levels.reverse
wenzelm
parents: 59305
diff changeset
   208
            (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
wenzelm
parents: 59305
diff changeset
   209
              resort(bots.head, top, top_down) :: bots)
wenzelm
parents: 59305
diff changeset
   210
          }
wenzelm
parents: 59305
diff changeset
   211
        val new_crossings = count_crossings(graph, new_levels)
wenzelm
parents: 59305
diff changeset
   212
        if (new_crossings < old_crossings)
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   213
          (new_levels, new_crossings)
59306
wenzelm
parents: 59305
diff changeset
   214
        else
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   215
          (old_levels, old_crossings)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   216
    }._1
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   217
  }
50469
wenzelm
parents: 50468
diff changeset
   218
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   219
  private 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
   220
  {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   221
    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
   222
    val buckets = new Array[Level](max_lev + 1)
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   223
    for (l <- 0 to max_lev) { buckets(l) = Nil }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   224
    for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   225
    buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   226
  }
50469
wenzelm
parents: 50468
diff changeset
   227
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   228
  private def count_crossings(graph: Graph, levels: List[Level]): Int =
59310
wenzelm
parents: 59307
diff changeset
   229
    levels.iterator.sliding(2).map {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   230
      case List(top, bot) =>
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   231
        top.iterator.zipWithIndex.map {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   232
          case (outer_parent, outer_parent_index) =>
59310
wenzelm
parents: 59307
diff changeset
   233
            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
wenzelm
parents: 59307
diff changeset
   234
              (0 until outer_parent_index).iterator.map(inner_parent =>
71592
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 67601
diff changeset
   235
                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 67601
diff changeset
   236
                  .count(inner_child => outer_child < inner_child)).sum).sum
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   237
        }.sum
59447
e7cbfe240078 complete pattern coverage, e.g. relevant for singleton graph;
wenzelm
parents: 59419
diff changeset
   238
      case _ => 0
59310
wenzelm
parents: 59307
diff changeset
   239
    }.sum
59302
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
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
  /** pendulum method **/
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
  /*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
   246
    calculating coordinates with the "pendulum method". A "region" is a
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   247
    group of vertices which "stick together".*/
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   248
  private class Region(val content: List[Vertex])
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   249
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   250
    def distance(metrics: Metrics, graph: Graph, that: Region): Double =
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   251
      vertex_left(graph, that.content.head) -
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   252
      vertex_right(graph, this.content.last) -
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   253
      metrics.gap
59302
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 deflection(graph: Graph, top_down: Boolean): Double =
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   256
      ((for (a <- content.iterator) yield {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   257
        val x = graph.get_node(a).x
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   258
        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
   259
        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
   260
      }).sum / content.length).round.toDouble
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   261
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   262
    def move(graph: Graph, dx: Double): Graph =
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   263
      if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   264
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   265
    def combine(that: Region): Region = new Region(content ::: that.content)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   266
  }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   267
59313
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   268
  private def pendulum(
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   269
    options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   270
  {
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   271
    def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] =
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   272
      level match {
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   273
        case r1 :: rest =>
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   274
          val rest1 = combine_regions(graph, top_down, rest)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   275
          rest1 match {
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   276
            case r2 :: rest2 =>
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   277
              val d1 = r1.deflection(graph, top_down)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   278
              val d2 = r2.deflection(graph, top_down)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   279
              if (// Do regions touch?
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   280
                  r1.distance(metrics, graph, r2) <= 0.0 &&
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   281
                  // Do they influence each other?
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   282
                  (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   283
                r1.combine(r2) :: rest2
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   284
              else r1 :: rest1
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   285
            case _ => r1 :: rest1
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   286
          }
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   287
        case _ => level
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   288
      }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   289
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   290
    def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
50469
wenzelm
parents: 50468
diff changeset
   291
    {
71592
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 67601
diff changeset
   292
      ((graph, false) /: level.indices) {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   293
        case ((graph, moved), i) =>
59263
03aedb32a763 misc tuning;
wenzelm
parents: 59262
diff changeset
   294
          val r = level(i)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   295
          val d = r.deflection(graph, top_down)
59316
wenzelm
parents: 59315
diff changeset
   296
          val dx =
73591
2dd1fd9112d9 tuned --- silence odd warning;
wenzelm
parents: 73587
diff changeset
   297
            if (d < 0.0 && i > 0) {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   298
              - (level(i - 1).distance(metrics, graph, r) min (- d))
73591
2dd1fd9112d9 tuned --- silence odd warning;
wenzelm
parents: 73587
diff changeset
   299
            }
2dd1fd9112d9 tuned --- silence odd warning;
wenzelm
parents: 73587
diff changeset
   300
            else if (d >= 0.0 && i < level.length - 1) {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   301
              r.distance(metrics, graph, level(i + 1)) min d
73591
2dd1fd9112d9 tuned --- silence odd warning;
wenzelm
parents: 73587
diff changeset
   302
            }
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   303
            else d
59316
wenzelm
parents: 59315
diff changeset
   304
          (r.move(graph, dx), moved || d != 0.0)
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   305
      }
50469
wenzelm
parents: 50468
diff changeset
   306
    }
wenzelm
parents: 50468
diff changeset
   307
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   308
    val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
50469
wenzelm
parents: 50468
diff changeset
   309
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   310
    ((levels_graph, initial_regions, true) /:
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   311
      (1 to (2 * options.int("graphview_iterations_pendulum")))) {
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   312
      case ((graph, regions, moved), iteration) =>
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   313
        val top_down = (iteration % 2 == 1)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   314
        if (moved) {
59315
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   315
          val (graph1, regions1, moved1) =
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   316
            ((graph, List.empty[List[Region]], false) /:
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   317
              (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   318
                val bot1 = combine_regions(graph, top_down, bot)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   319
                val (graph1, moved1) = deflect(bot1, top_down, graph)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   320
                (graph1, bot1 :: tops, moved || moved1)
2f4d64fba0d7 misc tuning;
wenzelm
parents: 59313
diff changeset
   321
            }
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   322
          (graph1, regions1.reverse, moved1)
59265
962ad3942ea7 more metrics, with integer coordinates for layout;
wenzelm
parents: 59264
diff changeset
   323
        }
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   324
        else (graph, regions, moved)
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   325
    }._1
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   326
  }
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   327
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   328
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   329
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   330
  /** rubberband method **/
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   331
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   332
  private def force_weight(graph: Graph, v: Vertex): Double =
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   333
  {
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   334
    val preds = graph.imm_preds(v)
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   335
    val succs = graph.imm_succs(v)
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   336
    val n = preds.size + succs.size
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   337
    if (n == 0) 0.0
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   338
    else {
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   339
      val x = graph.get_node(v).x
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   340
      ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   341
    }
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   342
  }
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   343
59313
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   344
  private def rubberband(
d7f4f46e9a59 configurable options;
wenzelm
parents: 59312
diff changeset
   345
    options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   346
  {
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   347
    val gap = metrics.gap
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   348
59419
2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
wenzelm
parents: 59384
diff changeset
   349
    (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   350
      (graph /: levels) { case (graph, level) =>
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   351
        val m = level.length - 1
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   352
        (graph /: level.iterator.zipWithIndex) {
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   353
          case (g, (v, i)) =>
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   354
            val d = force_weight(g, v)
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   355
            if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   356
                d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
59307
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   357
              move_vertex(g, v, d.round.toDouble)
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   358
            else g
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   359
        }
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   360
      }
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   361
    }
b5d1b8175b8e rubberband method as in old browser;
wenzelm
parents: 59306
diff changeset
   362
  }
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
   363
}
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   364
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   365
final class Layout private(
59290
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   366
  val metrics: Metrics,
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   367
  val input_graph: Graph_Display.Graph,
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   368
  val output_graph: Layout.Graph)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   369
{
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   370
  /* vertex coordinates */
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   371
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   372
  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
   373
  {
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   374
    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
   375
    else {
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   376
      val output_graph1 =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   377
        output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy))
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   378
      new Layout(metrics, input_graph, output_graph1)
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   379
    }
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   380
  }
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   381
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   382
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   383
  /* regular nodes */
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   385
  def get_node(node: Graph_Display.Node): Layout.Info =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   386
    output_graph.get_node(Layout.Node(node))
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   387
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   388
  def nodes_iterator: Iterator[Layout.Info] =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   389
    for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   390
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   391
59290
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   392
  /* dummies */
569a8109eeb2 separate module Metrics;
wenzelm
parents: 59265
diff changeset
   393
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   394
  def dummies_iterator: Iterator[Layout.Info] =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   395
    for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   396
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   397
  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   398
    new Iterator[Layout.Info] {
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   399
      private var index = 0
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   400
      def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
73587
0af9e7e4476f tuned --- fewer warnings;
wenzelm
parents: 71816
diff changeset
   401
      def next(): Layout.Info =
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   402
      {
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   403
        val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   404
        index += 1
59384
c75327a34960 more explicit Layout.Info: size and content;
wenzelm
parents: 59316
diff changeset
   405
        info
59302
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   406
      }
4d985afc0565 explict layout graph structure, with dummies and coordinates;
wenzelm
parents: 59292
diff changeset
   407
    }
59262
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   408
}
5cd92c743958 explicit Layout.Point;
wenzelm
parents: 59261
diff changeset
   409