# HG changeset patch
# User wenzelm
# Date 1568299924 -7200
# Node ID 41b5e515c238470f22cf41747d7969c3732405e4
# Parent  7e93a10b21f0f9c6654e56c9d6f19dbd7023f219
clarified signature: eliminated unused option;

diff -r 7e93a10b21f0 -r 41b5e515c238 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Sep 12 15:32:45 2019 +0100
+++ b/src/Pure/General/graph.scala	Thu Sep 12 16:52:04 2019 +0200
@@ -30,13 +30,10 @@
     new Graph[Key, A](SortedMap.empty(ord))
 
   def make[Key, A](entries: List[((Key, A), List[Key])],
-    symmetric: Boolean = false,
-    permissive: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
+    symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
-      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) =>
-        if (permissive) graph.default_node(x, info) else graph.new_node(x, info)
-      }
+      (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
     val graph2 =
       (graph1 /: entries) { case (graph, ((x, _), ys)) =>
         (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) }
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 = "")