# HG changeset patch
# User wenzelm
# Date 1567588867 -7200
# Node ID fa04b549f65273f804184816798390edee2f1e22
# Parent  9a40720750dc2bf45d4ded67ba7ebc8fb73333b9
tuned signature;

diff -r 9a40720750dc -r fa04b549f652 src/Pure/PIDE/document.scala
--- 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
diff -r 9a40720750dc -r fa04b549f652 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 03 19:20:22 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 04 11:21:07 2019 +0200
@@ -338,6 +338,10 @@
         case errs => error(cat_lines(errs))
       }
 
+    lazy val theory_graph: Document.Theory_Graph[A] =
+      Document.theory_graph(entries.map(entry =>
+        ((entry.name, seen(entry.name)), entry.header.imports)))
+
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
diff -r 9a40720750dc -r fa04b549f652 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 03 19:20:22 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Sep 04 11:21:07 2019 +0200
@@ -119,7 +119,7 @@
 
     def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
 
-    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
+    lazy val theory_graph: Document.Theory_Graph[Unit] =
       Document.theory_graph(
         for ((_, entry) <- theories.toList)
         yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)))
@@ -204,8 +204,8 @@
         name <- base.dump_checkpoints.iterator
       } yield name).toSet
 
-    def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
-      : Graph[Document.Node.Name, Options] =
+    def used_theories_condition(
+      default_options: Options, progress: Progress = No_Progress): Document.Theory_Graph[Options] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
       Document.theory_graph(