author  wenzelm 
Sun, 25 Jan 2015 17:17:37 +0100  
changeset 59440  07e3c15cb10c 
parent 59245  be4180f3c236 
child 66823  f529719cc47d 
permissions  rwrr 
59244  1 
/* Title: Pure/General/graph_display.scala 
2 
Author: Makarius 

3 

4 
Support for graph display. 

5 
*/ 

6 

7 
package isabelle 

8 

9 
object Graph_Display 

10 
{ 

11 
/* graph entries */ 

12 

59440  13 
type Entry = ((String, (String, XML.Body)), List[String]) // ident, name, content, parents 
59244  14 

15 

59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59244
diff
changeset

16 
/* graph structure */ 
59244  17 

59245
be4180f3c236
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
wenzelm
parents:
59244
diff
changeset

18 
object Node 
59244  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  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  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  27 
case ord => ord 
28 
} 

29 
} 

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  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  34 
override def toString: String = name 
35 
} 

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  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  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  42 

43 
def build_graph(entries: List[Entry]): Graph = 

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  48 
} 
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  51 
}) /: entries) { 
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  54 
} 
55 
} 

56 

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  63 
} 
64 