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