diff -r 7e93a10b21f0 -r 41b5e515c238 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Sep 12 15:32:45 2019 +0100 +++ b/src/Pure/PIDE/document.scala Thu Sep 12 16:52:04 2019 +0200 @@ -111,9 +111,8 @@ type Graph[A] = isabelle.Graph[Node.Name, A] - def make_graph[A]( - entries: List[((Name, A), List[Name])], permissive: Boolean = false): Graph[A] = - Graph.make(entries, symmetric = true, permissive = permissive)(Ordering) + def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] = + Graph.make(entries, symmetric = true)(Ordering) } sealed case class Name(node: String, master_dir: String = "", theory: String = "")