--- a/src/Pure/PIDE/resources.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Sun Nov 12 19:46:19 2017 +0100
@@ -249,7 +249,7 @@
new Dependencies(rev_entries, seen + name)
def entries: List[Document.Node.Entry] = rev_entries.reverse
- def names: List[Document.Node.Name] = entries.map(_.name)
+ def theories: List[Document.Node.Name] = entries.map(_.name)
def errors: List[String] = entries.flatMap(_.header.errors)
@@ -276,15 +276,15 @@
def loaded_files: List[(String, List[Path])] =
{
- names.map(_.theory) zip
+ theories.map(_.theory) zip
Par_List.map((e: () => List[Path]) => e(),
- names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+ theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
}
def imported_files: List[Path] =
{
val base_theories =
- loaded_theories.all_preds(names.map(_.theory)).
+ loaded_theories.all_preds(theories.map(_.theory)).
filter(session_base.loaded_theories.defined(_))
base_theories.map(theory => session_base.known.theories(theory).path) :::
--- a/src/Pure/Thy/sessions.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Sun Nov 12 19:46:19 2017 +0100
@@ -234,7 +234,7 @@
val overall_syntax = dependencies.overall_syntax
- val theory_files = dependencies.names.map(_.path)
+ val theory_files = dependencies.theories.map(_.path)
val loaded_files =
if (inlined_files) {
if (Sessions.is_pure(info.name)) {
@@ -294,7 +294,7 @@
val known =
Known.make(info.dir, List(imports_base),
- theories = dependencies.names,
+ theories = dependencies.theories,
loaded_files = loaded_files)
val sources_errors =
--- a/src/Pure/Thy/thy_resources.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala Sun Nov 12 19:46:19 2017 +0100
@@ -66,7 +66,7 @@
yield (import_name(qualifier, master_dir, thy), pos)
val dependencies = resources.dependencies(import_names).check_errors
- val loaded_theories = dependencies.names.map(read_thy(_))
+ val loaded_theories = dependencies.theories.map(read_thy(_))
val edits =
state.change_result(st =>
@@ -84,6 +84,6 @@
})
session.update(Document.Blobs.empty, edits)
- dependencies.names
+ dependencies.theories
}
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Nov 12 19:46:19 2017 +0100
@@ -208,7 +208,7 @@
(for ((_, model) <- st.models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
- val thy_files = dependencies(thys).names
+ val thy_files = dependencies(thys).theories
/* auxiliary files */
--- a/src/Tools/jEdit/src/document_model.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Nov 12 19:46:19 2017 +0100
@@ -253,7 +253,7 @@
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
- val retain = PIDE.resources.dependencies(imports).names.toSet
+ val retain = PIDE.resources.dependencies(imports).theories.toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit
--- a/src/Tools/jEdit/src/plugin.scala Sun Nov 12 19:42:22 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 12 19:46:19 2017 +0100
@@ -126,7 +126,7 @@
val thys =
(for ((node_name, model) <- models.iterator if model.is_theory)
yield (node_name, Position.none)).toList
- val thy_files = resources.dependencies(thys).names
+ val thy_files = resources.dependencies(thys).theories
val aux_files =
if (options.bool("jedit_auto_resolve")) {