tuned signature;
authorwenzelm
Sun Jan 08 17:42:31 2017 +0100 (2017-01-08)
changeset 64839842163abfc0d
parent 64838 ae6c51dcba9c
child 64840 d67253005c0c
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Jan 08 17:36:00 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Jan 08 17:42:31 2017 +0100
     1.3 @@ -26,6 +26,9 @@
     1.4    val base_syntax: Outer_Syntax,
     1.5    val log: Logger = No_Logger)
     1.6  {
     1.7 +  val thy_info = new Thy_Info(this)
     1.8 +
     1.9 +
    1.10    /* document node names */
    1.11  
    1.12    def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
     2.1 --- a/src/Pure/Tools/build.scala	Sun Jan 08 17:36:00 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sun Jan 08 17:42:31 2017 +0100
     2.3 @@ -137,7 +137,6 @@
     2.4                    (parent.loaded_theories, parent.known_theories, parent.syntax)
     2.5                }
     2.6              val resources = new Resources(loaded_theories0, known_theories0, syntax0)
     2.7 -            val thy_info = new Thy_Info(resources)
     2.8  
     2.9              if (verbose || list_files) {
    2.10                val groups =
    2.11 @@ -155,7 +154,7 @@
    2.12                        (resources.node_name(
    2.13                          if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
    2.14                  })
    2.15 -              val thy_deps = thy_info.dependencies(name, root_theories)
    2.16 +              val thy_deps = resources.thy_info.dependencies(name, root_theories)
    2.17  
    2.18                thy_deps.errors match {
    2.19                  case Nil => thy_deps
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 17:36:00 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 17:42:31 2017 +0100
     3.3 @@ -151,8 +151,6 @@
     3.4  
     3.5    /* resolve dependencies */
     3.6  
     3.7 -  val thy_info = new Thy_Info(this)
     3.8 -
     3.9    def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) =
    3.10    {
    3.11      state.change_result(st =>
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 17:36:00 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Jan 08 17:42:31 2017 +0100
     4.3 @@ -188,11 +188,9 @@
     4.4            val thys =
     4.5              (for ((node_name, model) <- models.iterator if model.is_theory)
     4.6                yield (node_name, Position.none)).toList
     4.7 +          val thy_files = PIDE.resources.thy_info.dependencies("", thys).deps.map(_.name)
     4.8  
     4.9 -          val thy_info = new Thy_Info(PIDE.resources)
    4.10 -          val thy_files: List[Document.Node.Name] = thy_info.dependencies("", thys).deps.map(_.name)
    4.11 -
    4.12 -          val aux_files: List[Document.Node.Name] =
    4.13 +          val aux_files =
    4.14              if (PIDE.options.bool("jedit_auto_resolve")) {
    4.15                val stable_tip_version =
    4.16                  if (models.forall(p => p._2.is_stable))