# HG changeset patch
# User wenzelm
# Date 1316280314 -7200
# Node ID b536b1144eb303bc5304c0c04192968d5f24307c
# Parent  cdfe42f1267c4f8232495f491ec9a2b366804c7b
more careful traversal of theory dependencies to retain standard import order;

diff -r cdfe42f1267c -r b536b1144eb3 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Sat Sep 17 17:55:39 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Sat Sep 17 19:25:14 2011 +0200
@@ -47,16 +47,19 @@
     Document.Node.Name(node, dir1, theory)
   }
 
-  type Deps = Map[Document.Node.Name, Document.Node_Header]
+  type Dep = (Document.Node.Name, Document.Node_Header)
+  private type Required = (List[Dep], Set[Document.Node.Name])
 
   private def require_thys(initiators: List[Document.Node.Name],
-      deps: Deps, names: List[Document.Node.Name]): Deps =
-    (deps /: names)(require_thy(initiators, _, _))
+      required: Required, names: List[Document.Node.Name]): Required =
+    (required /: names)(require_thy(initiators, _, _))
 
   private def require_thy(initiators: List[Document.Node.Name],
-      deps: Deps, name: Document.Node.Name): Deps =
+      required: Required, name: Document.Node.Name): Required =
   {
-    if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps
+    val (deps, seen) = required
+    if (seen(name)) required
+    else if (thy_load.is_loaded(name.theory)) (deps, seen + name)
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
@@ -68,12 +71,13 @@
                 quote(name.theory) + required_by(initiators))
           }
         val imports = header.imports.map(import_name(name.dir, _))
-        require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
+        val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports)
+        ((name, Exn.Res(header)) :: deps1, seen1)
       }
-      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+      catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
     }
   }
 
-  def dependencies(names: List[Document.Node.Name]): Deps =
-    require_thys(Nil, Map.empty, names)
+  def dependencies(names: List[Document.Node.Name]): List[Dep] =
+    require_thys(Nil, (Nil, Set.empty), names)._1.reverse
 }
diff -r cdfe42f1267c -r b536b1144eb3 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 17 17:55:39 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 17 19:25:14 2011 +0200
@@ -373,7 +373,7 @@
       val thys =
         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
           yield model.name
-      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
+      val files = thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
 
       if (!files.isEmpty) {
         val files_list = new ListView(Library.sort_strings(files))
@@ -388,8 +388,10 @@
             "Reload selected files now?",
             new ScrollPane(files_list))
         if (answer == 0)
-          files_list.selection.items foreach (file =>
-            if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
+          for {
+            file <- files
+            if !loaded_buffer(file) && files_list.selection.items.contains(file)
+          } jEdit.openFile(null: View, file)
       }
     }