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