# HG changeset patch
# User wenzelm
# Date 1567413674 -7200
# Node ID 4c98d37e14482ade91000989dd27649c608a5595
# Parent  a56eab490f4e9cbbb6de5114c58d190f1bde3123
prefer Theory_Ordering theory names are unique (due to proper session context);

diff -r a56eab490f4e -r 4c98d37e1448 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 01 22:57:25 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 02 10:41:14 2019 +0200
@@ -399,7 +399,7 @@
         val entries =
           for ((name, theory) <- theories.toList)
           yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
-        Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
+        Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
       }
 
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
diff -r a56eab490f4e -r 4c98d37e1448 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Sep 01 22:57:25 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 02 10:41:14 2019 +0200
@@ -124,7 +124,7 @@
       val entries =
         for ((_, entry) <- theories.toList)
         yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp._1.theory).name))
-      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
+      Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
     }
 
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =