11 /* graph entries */ |
11 /* graph entries */ |
12 |
12 |
13 type Entry = ((String, (String, XML.Body)), List[String]) |
13 type Entry = ((String, (String, XML.Body)), List[String]) |
14 |
14 |
15 |
15 |
16 /* node names */ |
16 /* graph structure */ |
17 |
17 |
18 object Name |
18 object Node |
19 { |
19 { |
20 val dummy: Name = Name("", "") |
20 val dummy: Node = Node("", "") |
21 |
21 |
22 object Ordering extends scala.math.Ordering[Name] |
22 object Ordering extends scala.math.Ordering[Node] |
23 { |
23 { |
24 def compare(name1: Name, name2: Name): Int = |
24 def compare(node1: Node, node2: Node): Int = |
25 name1.name compare name2.name match { |
25 node1.name compare node2.name match { |
26 case 0 => name1.ident compare name2.ident |
26 case 0 => node1.ident compare node2.ident |
27 case ord => ord |
27 case ord => ord |
28 } |
28 } |
29 } |
29 } |
30 } |
30 } |
31 |
31 sealed case class Node(name: String, ident: String) |
32 sealed case class Name(name: String, ident: String) |
|
33 { |
32 { |
|
33 def is_dummy: Boolean = this == Node.dummy |
34 override def toString: String = name |
34 override def toString: String = name |
35 } |
35 } |
36 |
36 |
|
37 type Edge = (Node, Node) |
37 |
38 |
38 /* graph structure */ |
39 type Graph = isabelle.Graph[Node, XML.Body] |
39 |
40 |
40 type Graph = isabelle.Graph[Name, XML.Body] |
41 val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering) |
41 |
|
42 val empty_graph: Graph = isabelle.Graph.empty(Name.Ordering) |
|
43 |
42 |
44 def build_graph(entries: List[Entry]): Graph = |
43 def build_graph(entries: List[Entry]): Graph = |
45 { |
44 { |
46 val the_key = |
45 val node = |
47 (Map.empty[String, Name] /: entries) { |
46 (Map.empty[String, Node] /: entries) { |
48 case (m, ((ident, (name, _)), _)) => m + (ident -> Name(name, ident)) |
47 case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident)) |
49 } |
48 } |
50 (((empty_graph /: entries) { |
49 (((empty_graph /: entries) { |
51 case (g, ((ident, (_, content)), _)) => g.new_node(the_key(ident), content) |
50 case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content) |
52 }) /: entries) { |
51 }) /: entries) { |
53 case (g1, ((ident, _), parents)) => |
52 case (g1, ((ident, _), parents)) => |
54 (g1 /: parents) { case (g2, parent) => g2.add_edge(the_key(parent), the_key(ident)) } |
53 (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) } |
55 } |
54 } |
56 } |
55 } |
57 |
56 |
58 def decode_graph(body: XML.Body): Graph = |
57 def decode_graph(body: XML.Body): Graph = |
59 { |
58 build_graph( |
60 val entries = |
59 { |
61 { |
60 import XML.Decode._ |
62 import XML.Decode._ |
61 list(pair(pair(string, pair(string, x => x)), list(string)))(body) |
63 list(pair(pair(string, pair(string, x => x)), list(string)))(body) |
62 }) |
64 } |
|
65 build_graph(entries) |
|
66 } |
|
67 } |
63 } |
68 |
64 |