src/Pure/General/graph_display.scala
author wenzelm
Sun, 25 Jan 2015 17:17:37 +0100
changeset 59440 07e3c15cb10c
parent 59245 be4180f3c236
child 66823 f529719cc47d
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/graph_display.scala
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     3
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     4
Support for graph display.
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     5
*/
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     6
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     8
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
     9
object Graph_Display
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    10
{
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    11
  /* graph entries */
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    12
59440
07e3c15cb10c tuned comments;
wenzelm
parents: 59245
diff changeset
    13
  type Entry = ((String, (String, XML.Body)), List[String])  // ident, name, content, parents
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    14
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    15
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    16
  /* graph structure */
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    17
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    18
  object Node
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    19
  {
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    20
    val dummy: Node = Node("", "")
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    21
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    22
    object Ordering extends scala.math.Ordering[Node]
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    23
    {
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    24
      def compare(node1: Node, node2: Node): Int =
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    25
        node1.name compare node2.name match {
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    26
          case 0 => node1.ident compare node2.ident
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    27
          case ord => ord
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    28
        }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    29
    }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    30
  }
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    31
  sealed case class Node(name: String, ident: String)
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    32
  {
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    33
    def is_dummy: Boolean = this == Node.dummy
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    34
    override def toString: String = name
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    35
  }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    36
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    37
  type Edge = (Node, Node)
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    38
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    39
  type Graph = isabelle.Graph[Node, XML.Body]
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    40
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    41
  val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering)
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    42
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    43
  def build_graph(entries: List[Entry]): Graph =
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    44
  {
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    45
    val node =
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    46
      (Map.empty[String, Node] /: entries) {
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    47
        case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    48
      }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    49
    (((empty_graph /: entries) {
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    50
        case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    51
      }) /: entries) {
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    52
        case (g1, ((ident, _), parents)) =>
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    53
          (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    54
      }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    55
  }
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    56
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    57
  def decode_graph(body: XML.Body): Graph =
59245
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    58
    build_graph(
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    59
      {
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    60
        import XML.Decode._
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    61
        list(pair(pair(string, pair(string, x => x)), list(string)))(body)
be4180f3c236 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents: 59244
diff changeset
    62
      })
59244
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    63
}
19b5fc4b2b38 more uniform support for graph display in ML/Scala;
wenzelm
parents:
diff changeset
    64