tuned signature;
authorwenzelm
Sun Nov 12 19:46:19 2017 +0100 (3 months ago)
changeset 67059df7d728103f1
parent 67058 03d4954c68bb
child 67060 9ad7bf553ee1
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_resources.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Nov 12 19:42:22 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 19:46:19 2017 +0100
     1.3 @@ -249,7 +249,7 @@
     1.4        new Dependencies(rev_entries, seen + name)
     1.5  
     1.6      def entries: List[Document.Node.Entry] = rev_entries.reverse
     1.7 -    def names: List[Document.Node.Name] = entries.map(_.name)
     1.8 +    def theories: List[Document.Node.Name] = entries.map(_.name)
     1.9  
    1.10      def errors: List[String] = entries.flatMap(_.header.errors)
    1.11  
    1.12 @@ -276,15 +276,15 @@
    1.13  
    1.14      def loaded_files: List[(String, List[Path])] =
    1.15      {
    1.16 -      names.map(_.theory) zip
    1.17 +      theories.map(_.theory) zip
    1.18          Par_List.map((e: () => List[Path]) => e(),
    1.19 -          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    1.20 +          theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    1.21      }
    1.22  
    1.23      def imported_files: List[Path] =
    1.24      {
    1.25        val base_theories =
    1.26 -        loaded_theories.all_preds(names.map(_.theory)).
    1.27 +        loaded_theories.all_preds(theories.map(_.theory)).
    1.28            filter(session_base.loaded_theories.defined(_))
    1.29  
    1.30        base_theories.map(theory => session_base.known.theories(theory).path) :::
     2.1 --- a/src/Pure/Thy/sessions.scala	Sun Nov 12 19:42:22 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 19:46:19 2017 +0100
     2.3 @@ -234,7 +234,7 @@
     2.4  
     2.5              val overall_syntax = dependencies.overall_syntax
     2.6  
     2.7 -            val theory_files = dependencies.names.map(_.path)
     2.8 +            val theory_files = dependencies.theories.map(_.path)
     2.9              val loaded_files =
    2.10                if (inlined_files) {
    2.11                  if (Sessions.is_pure(info.name)) {
    2.12 @@ -294,7 +294,7 @@
    2.13  
    2.14              val known =
    2.15                Known.make(info.dir, List(imports_base),
    2.16 -                theories = dependencies.names,
    2.17 +                theories = dependencies.theories,
    2.18                  loaded_files = loaded_files)
    2.19  
    2.20              val sources_errors =
     3.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:42:22 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:46:19 2017 +0100
     3.3 @@ -66,7 +66,7 @@
     3.4        yield (import_name(qualifier, master_dir, thy), pos)
     3.5  
     3.6      val dependencies = resources.dependencies(import_names).check_errors
     3.7 -    val loaded_theories = dependencies.names.map(read_thy(_))
     3.8 +    val loaded_theories = dependencies.theories.map(read_thy(_))
     3.9  
    3.10      val edits =
    3.11        state.change_result(st =>
    3.12 @@ -84,6 +84,6 @@
    3.13        })
    3.14      session.update(Document.Blobs.empty, edits)
    3.15  
    3.16 -    dependencies.names
    3.17 +    dependencies.theories
    3.18    }
    3.19  }
     4.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Nov 12 19:42:22 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Nov 12 19:46:19 2017 +0100
     4.3 @@ -208,7 +208,7 @@
     4.4            (for ((_, model) <- st.models.iterator if model.is_theory)
     4.5             yield (model.node_name, Position.none)).toList
     4.6  
     4.7 -        val thy_files = dependencies(thys).names
     4.8 +        val thy_files = dependencies(thys).theories
     4.9  
    4.10  
    4.11          /* auxiliary files */
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 12 19:42:22 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 12 19:46:19 2017 +0100
     5.3 @@ -253,7 +253,7 @@
     5.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
     5.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
     5.6              }
     5.7 -            val retain = PIDE.resources.dependencies(imports).names.toSet
     5.8 +            val retain = PIDE.resources.dependencies(imports).theories.toSet
     5.9  
    5.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
    5.11                yield edit
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 12 19:42:22 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 12 19:46:19 2017 +0100
     6.3 @@ -126,7 +126,7 @@
     6.4            val thys =
     6.5              (for ((node_name, model) <- models.iterator if model.is_theory)
     6.6                yield (node_name, Position.none)).toList
     6.7 -          val thy_files = resources.dependencies(thys).names
     6.8 +          val thy_files = resources.dependencies(thys).theories
     6.9  
    6.10            val aux_files =
    6.11              if (options.bool("jedit_auto_resolve")) {