equal
deleted
inserted
replaced
74 |
74 |
75 type Edit[A, B] = (Node.Name, Node.Edit[A, B]) |
75 type Edit[A, B] = (Node.Name, Node.Edit[A, B]) |
76 type Edit_Text = Edit[Text.Edit, Text.Perspective] |
76 type Edit_Text = Edit[Text.Edit, Text.Perspective] |
77 type Edit_Command = Edit[Command.Edit, Command.Perspective] |
77 type Edit_Command = Edit[Command.Edit, Command.Perspective] |
78 |
78 |
|
79 type Theory_Graph[A] = Graph[Node.Name, A] |
|
80 |
79 def theory_graph[A]( |
81 def theory_graph[A]( |
80 entries: List[((Node.Name, A), List[Node.Name])], |
82 entries: List[((Node.Name, A), List[Node.Name])], |
81 permissive: Boolean = false): Graph[Node.Name, A] = |
83 permissive: Boolean = false): Theory_Graph[A] = |
82 Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering) |
84 Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering) |
83 |
85 |
84 object Node |
86 object Node |
85 { |
87 { |
86 /* header and name */ |
88 /* header and name */ |