equal
deleted
inserted
replaced
73 /* document nodes: theories and auxiliary files */ |
73 /* document nodes: theories and auxiliary files */ |
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 |
|
79 def theory_graph[A]( |
|
80 entries: List[((Node.Name, A), List[Node.Name])], |
|
81 permissive: Boolean = false): Graph[Node.Name, A] = |
|
82 Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering) |
78 |
83 |
79 object Node |
84 object Node |
80 { |
85 { |
81 /* header and name */ |
86 /* header and name */ |
82 |
87 |