--- 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
--- 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
--- 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(