# HG changeset patch
# User wenzelm
# Date 1567940823 -7200
# Node ID 29bb1ebb188f82b92b8d10c7c227257865de1623
# Parent  b0172698d0d35abb029c8988685aacf66174d972
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

diff -r b0172698d0d3 -r 29bb1ebb188f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Sep 07 19:52:36 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 08 13:07:03 2019 +0200
@@ -76,13 +76,6 @@
   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): Theory_Graph[A] =
-    Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering)
-
   object Node
   {
     /* header and name */
@@ -116,10 +109,11 @@
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
 
-      object Theory_Ordering extends scala.math.Ordering[Name]
-      {
-        def compare(name1: Name, name2: Name): Int = name1.theory compare name2.theory
-      }
+      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)
     }
 
     sealed case class Name(node: String, master_dir: String = "", theory: String = "")
diff -r b0172698d0d3 -r 29bb1ebb188f src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Sep 07 19:52:36 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 08 13:07:03 2019 +0200
@@ -63,7 +63,7 @@
     nodes: List[Document.Node.Name])
   {
     def next(
-      dep_graph: Document.Theory_Graph[Unit],
+      dep_graph: Document.Node.Name.Graph[Unit],
       finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Checkpoints_State) =
     {
       import Checkpoints_State.Status
@@ -150,7 +150,7 @@
       already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
       result: Option[Exn.Result[Use_Theories_Result]] = None)
     {
-      def dep_graph: Document.Theory_Graph[Unit] = dependencies.theory_graph
+      def dep_graph: Document.Node.Name.Graph[Unit] = dependencies.theory_graph
 
       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
         copy(last_update = Time.now(), nodes_status = new_nodes_status)
@@ -479,8 +479,8 @@
 
       /* theories */
 
-      lazy val theory_graph: Document.Theory_Graph[Unit] =
-        Document.theory_graph(
+      lazy val theory_graph: Document.Node.Name.Graph[Unit] =
+        Document.Node.Name.make_graph(
           for ((name, theory) <- theories.toList)
           yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
 
diff -r b0172698d0d3 -r 29bb1ebb188f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Sep 07 19:52:36 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Sun Sep 08 13:07:03 2019 +0200
@@ -348,7 +348,7 @@
         case errs => error(cat_lines(errs))
       }
 
-    lazy val theory_graph: Document.Theory_Graph[Unit] =
+    lazy val theory_graph: Document.Node.Name.Graph[Unit] =
     {
       val regular = theories.toSet
       val irregular =
@@ -358,7 +358,7 @@
           if !regular(imp)
         } yield imp).toSet
 
-      Document.theory_graph(
+      Document.Node.Name.make_graph(
         irregular.toList.map(name => ((name, ()), Nil)) :::
         entries.map(entry => ((entry.name, ()), entry.header.imports)))
     }
diff -r b0172698d0d3 -r 29bb1ebb188f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 07 19:52:36 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Sep 08 13:07:03 2019 +0200
@@ -119,8 +119,8 @@
 
     def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
 
-    lazy val theory_graph: Document.Theory_Graph[Unit] =
-      Document.theory_graph(
+    lazy val theory_graph: Document.Node.Name.Graph[Unit] =
+      Document.Node.Name.make_graph(
         for ((_, entry) <- theories.toList)
         yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)))
 
@@ -209,11 +209,11 @@
         name <- base.dump_checkpoints.iterator
       } yield name).toSet
 
-    def used_theories_condition(
-      default_options: Options, progress: Progress = No_Progress): Document.Theory_Graph[Options] =
+    def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
+      : Document.Node.Name.Graph[Options] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
-      Document.theory_graph(
+      Document.Node.Name.make_graph(
         permissive = true,
         entries =
           for {