# HG changeset patch # User wenzelm # Date 1483893751 -3600 # Node ID 842163abfc0dfe4b3df794f26286cb00f102d73c # Parent ae6c51dcba9c643e56fada1cd6c1fa0b915dd1c2 tuned signature; diff -r ae6c51dcba9c -r 842163abfc0d src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sun Jan 08 17:36:00 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Jan 08 17:42:31 2017 +0100 @@ -26,6 +26,9 @@ val base_syntax: Outer_Syntax, val log: Logger = No_Logger) { + val thy_info = new Thy_Info(this) + + /* document node names */ def node_name(qualifier: String, raw_path: Path): Document.Node.Name = diff -r ae6c51dcba9c -r 842163abfc0d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Jan 08 17:36:00 2017 +0100 +++ b/src/Pure/Tools/build.scala Sun Jan 08 17:42:31 2017 +0100 @@ -137,7 +137,6 @@ (parent.loaded_theories, parent.known_theories, parent.syntax) } val resources = new Resources(loaded_theories0, known_theories0, syntax0) - val thy_info = new Thy_Info(resources) if (verbose || list_files) { val groups = @@ -155,7 +154,7 @@ (resources.node_name( if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos)) }) - val thy_deps = thy_info.dependencies(name, root_theories) + val thy_deps = resources.thy_info.dependencies(name, root_theories) thy_deps.errors match { case Nil => thy_deps diff -r ae6c51dcba9c -r 842163abfc0d src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 17:36:00 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 17:42:31 2017 +0100 @@ -151,8 +151,6 @@ /* resolve dependencies */ - val thy_info = new Thy_Info(this) - def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => diff -r ae6c51dcba9c -r 842163abfc0d src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Jan 08 17:36:00 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sun Jan 08 17:42:31 2017 +0100 @@ -188,11 +188,9 @@ val thys = (for ((node_name, model) <- models.iterator if model.is_theory) yield (node_name, Position.none)).toList + val thy_files = PIDE.resources.thy_info.dependencies("", thys).deps.map(_.name) - val thy_info = new Thy_Info(PIDE.resources) - val thy_files: List[Document.Node.Name] = thy_info.dependencies("", thys).deps.map(_.name) - - val aux_files: List[Document.Node.Name] = + val aux_files = if (PIDE.options.bool("jedit_auto_resolve")) { val stable_tip_version = if (models.forall(p => p._2.is_stable))