# HG changeset patch
# User wenzelm
# Date 1567517044 -7200
# Node ID 3047b76712798d6ee02474a33730e2194aea428e
# Parent  a4d265a6c5cc5c0bb2b5b1b23f6a2e16c7afb732
tuned signature;

diff -r a4d265a6c5cc -r 3047b7671279 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Sep 03 14:58:29 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 03 15:24:04 2019 +0200
@@ -76,6 +76,11 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
+  def theory_graph[A](
+      entries: List[((Node.Name, A), List[Node.Name])],
+      permissive: Boolean = false): Graph[Node.Name, A] =
+    Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering)
+
   object Node
   {
     /* header and name */
diff -r a4d265a6c5cc -r 3047b7671279 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Sep 03 14:58:29 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Sep 03 15:24:04 2019 +0200
@@ -399,12 +399,9 @@
       /* theories */
 
       lazy val theory_graph: Graph[Document.Node.Name, Unit] =
-      {
-        val entries =
+        Document.theory_graph(
           for ((name, theory) <- theories.toList)
-          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_)))
-        Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
-      }
+          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
 
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
 
diff -r a4d265a6c5cc -r 3047b7671279 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 03 14:58:29 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 03 15:24:04 2019 +0200
@@ -120,12 +120,9 @@
     def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
 
     lazy val theory_graph: Graph[Document.Node.Name, Unit] =
-    {
-      val entries =
+      Document.theory_graph(
         for ((_, entry) <- theories.toList)
-        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name))
-      Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
-    }
+        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)))
 
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
     {
@@ -211,30 +208,30 @@
       : Graph[Document.Node.Name, Options] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
-      val used =
-        for {
-          session_name <- sessions_structure.build_topological_order
-          entry @ ((name, options), _) <- session_bases(session_name).used_theories
-          if {
-            def warn(msg: String): Unit =
-              progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
+      Document.theory_graph(
+        permissive = true,
+        entries =
+          for {
+            session_name <- sessions_structure.build_topological_order
+            entry @ ((name, options), _) <- session_bases(session_name).used_theories
+            if {
+              def warn(msg: String): Unit =
+                progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
 
-            val conditions =
-              space_explode(',', options.string("condition")).
-                filter(cond => Isabelle_System.getenv(cond) == "")
-            if (conditions.nonEmpty) {
-              warn("undefined " + conditions.mkString(", "))
-              false
+              val conditions =
+                space_explode(',', options.string("condition")).
+                  filter(cond => Isabelle_System.getenv(cond) == "")
+              if (conditions.nonEmpty) {
+                warn("undefined " + conditions.mkString(", "))
+                false
+              }
+              else if (default_skip_proofs && !options.bool("skip_proofs")) {
+                warn("option skip_proofs")
+                false
+              }
+              else true
             }
-            else if (default_skip_proofs && !options.bool("skip_proofs")) {
-              warn("option skip_proofs")
-              false
-            }
-            else true
-          }
-        } yield entry
-      Graph.make[Document.Node.Name, Options](used, symmetric = true, permissive = true)(
-        Document.Node.Name.Theory_Ordering)
+          } yield entry)
     }
 
     def sources(name: String): List[SHA1.Digest] =