more careful traversal of theory dependencies to retain standard import order;
authorwenzelm
Sat Sep 17 19:25:14 2011 +0200 (2011-09-17)
changeset 44954b536b1144eb3
parent 44953 cdfe42f1267c
child 44955 9adaf5cd4f1c
more careful traversal of theory dependencies to retain standard import order;
src/Pure/Thy/thy_info.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/Thy/thy_info.scala	Sat Sep 17 17:55:39 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Sep 17 19:25:14 2011 +0200
     1.3 @@ -47,16 +47,19 @@
     1.4      Document.Node.Name(node, dir1, theory)
     1.5    }
     1.6  
     1.7 -  type Deps = Map[Document.Node.Name, Document.Node_Header]
     1.8 +  type Dep = (Document.Node.Name, Document.Node_Header)
     1.9 +  private type Required = (List[Dep], Set[Document.Node.Name])
    1.10  
    1.11    private def require_thys(initiators: List[Document.Node.Name],
    1.12 -      deps: Deps, names: List[Document.Node.Name]): Deps =
    1.13 -    (deps /: names)(require_thy(initiators, _, _))
    1.14 +      required: Required, names: List[Document.Node.Name]): Required =
    1.15 +    (required /: names)(require_thy(initiators, _, _))
    1.16  
    1.17    private def require_thy(initiators: List[Document.Node.Name],
    1.18 -      deps: Deps, name: Document.Node.Name): Deps =
    1.19 +      required: Required, name: Document.Node.Name): Required =
    1.20    {
    1.21 -    if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps
    1.22 +    val (deps, seen) = required
    1.23 +    if (seen(name)) required
    1.24 +    else if (thy_load.is_loaded(name.theory)) (deps, seen + name)
    1.25      else {
    1.26        try {
    1.27          if (initiators.contains(name)) error(cycle_msg(initiators))
    1.28 @@ -68,12 +71,13 @@
    1.29                  quote(name.theory) + required_by(initiators))
    1.30            }
    1.31          val imports = header.imports.map(import_name(name.dir, _))
    1.32 -        require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
    1.33 +        val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports)
    1.34 +        ((name, Exn.Res(header)) :: deps1, seen1)
    1.35        }
    1.36 -      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    1.37 +      catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
    1.38      }
    1.39    }
    1.40  
    1.41 -  def dependencies(names: List[Document.Node.Name]): Deps =
    1.42 -    require_thys(Nil, Map.empty, names)
    1.43 +  def dependencies(names: List[Document.Node.Name]): List[Dep] =
    1.44 +    require_thys(Nil, (Nil, Set.empty), names)._1.reverse
    1.45  }
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 17 17:55:39 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 17 19:25:14 2011 +0200
     2.3 @@ -373,7 +373,7 @@
     2.4        val thys =
     2.5          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
     2.6            yield model.name
     2.7 -      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
     2.8 +      val files = thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
     2.9  
    2.10        if (!files.isEmpty) {
    2.11          val files_list = new ListView(Library.sort_strings(files))
    2.12 @@ -388,8 +388,10 @@
    2.13              "Reload selected files now?",
    2.14              new ScrollPane(files_list))
    2.15          if (answer == 0)
    2.16 -          files_list.selection.items foreach (file =>
    2.17 -            if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
    2.18 +          for {
    2.19 +            file <- files
    2.20 +            if !loaded_buffer(file) && files_list.selection.items.contains(file)
    2.21 +          } jEdit.openFile(null: View, file)
    2.22        }
    2.23      }
    2.24