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")) {