# 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) } }