1/*  Title:      Pure/General/graph_display.scala
2    Author:     Makarius
3
4Support for graph display.
5*/
6
7package isabelle
8
9object Graph_Display
10{
11  /* graph entries */
12
13  type Entry = ((String, (String, XML.Body)), List[String])  // ident, name, content, parents
14
15
16  /* graph structure */
17
18  object Node
19  {
20    val dummy: Node = Node("", "")
21
22    object Ordering extends scala.math.Ordering[Node]
23    {
24      def compare(node1: Node, node2: Node): Int =
25        node1.name compare node2.name match {
26          case 0 => node1.ident compare node2.ident
27          case ord => ord
28        }
29    }
30  }
31  sealed case class Node(name: String, ident: String)
32  {
33    def is_dummy: Boolean = this == Node.dummy
34    override def toString: String = name
35  }
36
37  type Edge = (Node, Node)
38
39  type Graph = isabelle.Graph[Node, XML.Body]
40
41  val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering)
42
43  def build_graph(entries: List[Entry]): Graph =
44  {
45    val node =
46      (Map.empty[String, Node] /: entries) {
47        case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
48      }
49    (((empty_graph /: entries) {
50        case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
51      }) /: entries) {
52        case (g1, ((ident, _), parents)) =>
53          (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
54      }
55  }
56
57  def decode_graph(body: XML.Body): Graph =
58    build_graph(
59      {
60        import XML.Decode._
61        list(pair(pair(string, pair(string, x => x)), list(string)))(body)
62      })
63
64  def make_graph[A](
65    graph: isabelle.Graph[String, A],
66    isolated: Boolean = false,
67    name: (String, A) => String = (x: String, a: A) => x): Graph =
68  {
69    val entries =
70      (for { (x, (a, (ps, _))) <- graph.iterator if isolated || !graph.is_isolated(x) }
71       yield ((x, (name(x, a), Nil)), ps.toList)).toList
72    build_graph(entries)
73  }
74}
75