# HG changeset patch
# User wenzelm
# Date 1527597954 -7200
# Node ID 938803796a8b317449a24fa36e59a37b14e38c70
# Parent  a1e5de3681f0432b3fa711535eebcc51db83c474
tuned;

diff -r a1e5de3681f0 -r 938803796a8b src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue May 29 14:38:32 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue May 29 14:45:54 2018 +0200
@@ -300,7 +300,7 @@
   private def require_thy(
     progress: Progress,
     initiators: List[Document.Node.Name],
-    required: Dependencies,
+    dependencies: Dependencies,
     thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, pos) = thy
@@ -309,10 +309,10 @@
       "The error(s) above occurred for theory " + quote(name.theory) +
         required_by(initiators) + Position.here(pos)
 
-    if (required.seen(name)) required
+    if (dependencies.seen(name)) dependencies
     else {
-      val required1 = required + name
-      if (session_base.loaded_theory(name)) required1
+      val dependencies1 = dependencies + name
+      if (session_base.loaded_theory(name)) dependencies1
       else {
         try {
           if (initiators.contains(name)) error(cycle_msg(initiators))
@@ -322,11 +322,11 @@
             try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
             catch { case ERROR(msg) => cat_error(msg, message) }
           Document.Node.Entry(name, header) ::
-            require_thys(progress, name :: initiators, required1, header.imports)
+            require_thys(progress, name :: initiators, dependencies1, header.imports)
         }
         catch {
           case e: Throwable =>
-            Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+            Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: dependencies1
         }
       }
     }
@@ -335,9 +335,9 @@
   private def require_thys(
       progress: Progress,
       initiators: List[Document.Node.Name],
-      required: Dependencies,
+      dependencies: Dependencies,
       thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    (required /: thys)(require_thy(progress, initiators, _, _))
+    (dependencies /: thys)(require_thy(progress, initiators, _, _))
 
   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],