--- a/src/Pure/PIDE/document.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Pure/PIDE/document.scala Fri Sep 29 17:28:44 2017 +0200
@@ -126,6 +126,11 @@
def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
}
+ sealed case class Entry(name: Node.Name, header: Node.Header)
+ {
+ override def toString: String = name.toString
+ }
+
/* node overlays */
--- a/src/Pure/Thy/sessions.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Sep 29 17:28:44 2017 +0200
@@ -205,7 +205,7 @@
val syntax = thy_deps.syntax
- val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
+ val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node))
val loaded_files =
if (inlined_files) {
if (Sessions.is_pure(info.name)) {
@@ -251,18 +251,18 @@
val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
- (graph0 /: thy_deps.deps)(
- { case (g, dep) =>
- val a = node(dep.name)
+ (graph0 /: thy_deps.entries)(
+ { case (g, entry) =>
+ val a = node(entry.name)
val bs =
- dep.header.imports.map({ case (name, _) => node(name) }).
+ entry.header.imports.map({ case (name, _) => node(name) }).
filterNot(_ == a)
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
}
val known =
Known.make(info.dir, List(imports_base),
- theories = thy_deps.deps.map(_.name),
+ theories = thy_deps.entries.map(_.name),
loaded_files = loaded_files)
val sources =
--- a/src/Pure/Thy/thy_info.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 17:28:44 2017 +0200
@@ -7,18 +7,6 @@
package isabelle
-object Thy_Info
-{
- /* dependencies */
-
- sealed case class Dep(
- name: Document.Node.Name,
- header: Document.Node.Header)
- {
- override def toString: String = name.toString
- }
-}
-
class Thy_Info(resources: Resources)
{
/* messages */
@@ -42,36 +30,39 @@
}
final class Dependencies private(
- rev_deps: List[Thy_Info.Dep],
+ rev_entries: List[Document.Node.Entry],
val keywords: Thy_Header.Keywords,
val abbrevs: Thy_Header.Abbrevs,
val seen: Set[Document.Node.Name])
{
- def :: (dep: Thy_Info.Dep): Dependencies =
+ def :: (entry: Document.Node.Entry): Dependencies =
new Dependencies(
- dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, seen)
+ entry :: rev_entries,
+ entry.header.keywords ::: keywords,
+ entry.header.abbrevs ::: abbrevs,
+ seen)
def + (name: Document.Node.Name): Dependencies =
- new Dependencies(rev_deps, keywords, abbrevs, seen + name)
+ new Dependencies(rev_entries, keywords, abbrevs, seen + name)
- def deps: List[Thy_Info.Dep] = rev_deps.reverse
+ def entries: List[Document.Node.Entry] = rev_entries.reverse
- def errors: List[String] = deps.flatMap(dep => dep.header.errors)
+ def errors: List[String] = entries.flatMap(_.header.errors)
lazy val syntax: Outer_Syntax =
resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
def loaded_theories: Set[String] =
- resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory)
+ resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
def loaded_files: List[(String, List[Path])] =
{
- val names = deps.map(_.name)
+ val names = entries.map(_.name)
names.map(_.theory) zip
Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
}
- override def toString: String = deps.toString
+ override def toString: String = entries.toString
}
private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
@@ -96,11 +87,12 @@
val header =
try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
- Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
+ Document.Node.Entry(name, header) ::
+ require_thys(name :: initiators, required1, header.imports)
}
catch {
case e: Throwable =>
- Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
+ Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
}
}
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 17:28:44 2017 +0200
@@ -216,7 +216,7 @@
(for ((_, model) <- st.models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
- val thy_files = thy_info.dependencies(thys).deps.map(_.name)
+ val thy_files = thy_info.dependencies(thys).entries.map(_.name)
/* auxiliary files */
--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:28:44 2017 +0200
@@ -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.thy_info.dependencies(imports).deps.map(_.name).toSet
+ val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit
--- a/src/Tools/jEdit/src/plugin.scala Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 29 17:28:44 2017 +0200
@@ -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.thy_info.dependencies(thys).deps.map(_.name)
+ val thy_files = resources.thy_info.dependencies(thys).entries.map(_.name)
val aux_files =
if (options.bool("jedit_auto_resolve")) {