tuned;
authorwenzelm
Fri Sep 29 17:35:09 2017 +0200 (19 months ago)
changeset 667156bced18e2b91
parent 66714 9fc4e144693c
child 66716 8737b866bd1c
tuned;
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.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/Thy/sessions.scala	Fri Sep 29 17:28:44 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:35:09 2017 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4  
     1.5              val syntax = thy_deps.syntax
     1.6  
     1.7 -            val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node))
     1.8 +            val theory_files = thy_deps.names.map(name => Path.explode(name.node))
     1.9              val loaded_files =
    1.10                if (inlined_files) {
    1.11                  if (Sessions.is_pure(info.name)) {
    1.12 @@ -262,7 +262,7 @@
    1.13  
    1.14              val known =
    1.15                Known.make(info.dir, List(imports_base),
    1.16 -                theories = thy_deps.entries.map(_.name),
    1.17 +                theories = thy_deps.names,
    1.18                  loaded_files = loaded_files)
    1.19  
    1.20              val sources =
     2.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:28:44 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:35:09 2017 +0200
     2.3 @@ -46,6 +46,7 @@
     2.4        new Dependencies(rev_entries, keywords, abbrevs, seen + name)
     2.5  
     2.6      def entries: List[Document.Node.Entry] = rev_entries.reverse
     2.7 +    def names: List[Document.Node.Name] = entries.map(_.name)
     2.8  
     2.9      def errors: List[String] = entries.flatMap(_.header.errors)
    2.10  
    2.11 @@ -57,7 +58,6 @@
    2.12  
    2.13      def loaded_files: List[(String, List[Path])] =
    2.14      {
    2.15 -      val names = entries.map(_.name)
    2.16        names.map(_.theory) zip
    2.17          Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    2.18      }
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:28:44 2017 +0200
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 17:35:09 2017 +0200
     3.3 @@ -216,7 +216,7 @@
     3.4            (for ((_, model) <- st.models.iterator if model.is_theory)
     3.5             yield (model.node_name, Position.none)).toList
     3.6  
     3.7 -        val thy_files = thy_info.dependencies(thys).entries.map(_.name)
     3.8 +        val thy_files = thy_info.dependencies(thys).names
     3.9  
    3.10  
    3.11          /* auxiliary files */
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:28:44 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 17:35:09 2017 +0200
     4.3 @@ -253,7 +253,7 @@
     4.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
     4.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
     4.6              }
     4.7 -            val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet
     4.8 +            val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
     4.9  
    4.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
    4.11                yield edit
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:28:44 2017 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 17:35:09 2017 +0200
     5.3 @@ -126,7 +126,7 @@
     5.4            val thys =
     5.5              (for ((node_name, model) <- models.iterator if model.is_theory)
     5.6                yield (node_name, Position.none)).toList
     5.7 -          val thy_files = resources.thy_info.dependencies(thys).entries.map(_.name)
     5.8 +          val thy_files = resources.thy_info.dependencies(thys).names
     5.9  
    5.10            val aux_files =
    5.11              if (options.bool("jedit_auto_resolve")) {