--- a/src/Pure/PIDE/document.scala Tue Sep 03 19:20:22 2019 +0200
+++ b/src/Pure/PIDE/document.scala Wed Sep 04 11:21:07 2019 +0200
@@ -76,9 +76,11 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[Command.Edit, Command.Perspective]
+ type Theory_Graph[A] = Graph[Node.Name, A]
+
def theory_graph[A](
entries: List[((Node.Name, A), List[Node.Name])],
- permissive: Boolean = false): Graph[Node.Name, A] =
+ permissive: Boolean = false): Theory_Graph[A] =
Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering)
object Node