--- a/src/Pure/PIDE/resources.scala Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Tue Oct 31 15:55:50 2017 +0100
@@ -17,7 +17,7 @@
val session_base: Sessions.Base,
val log: Logger = No_Logger)
{
- val thy_info = new Thy_Info(this)
+ resources =>
def thy_path(path: Path): Path = path.ext("thy")
@@ -213,7 +213,113 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text]): Session.Change =
- Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
+ Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits)
def commit(change: Session.Change) { }
+
+
+ /* theory and file dependencies */
+
+ object Dependencies
+ {
+ val empty = new Dependencies(Nil, Set.empty)
+ }
+
+ final class Dependencies private(
+ rev_entries: List[Document.Node.Entry],
+ val seen: Set[Document.Node.Name])
+ {
+ def :: (entry: Document.Node.Entry): Dependencies =
+ new Dependencies(entry :: rev_entries, seen)
+
+ def + (name: Document.Node.Name): Dependencies =
+ 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 errors: List[String] = entries.flatMap(_.header.errors)
+
+ lazy val loaded_theories: Graph[String, Outer_Syntax] =
+ (session_base.loaded_theories /: entries)({ case (graph, entry) =>
+ val name = entry.name.theory
+ val imports = entry.header.imports.map(p => p._1.theory)
+
+ val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
+ val graph2 = (graph1 /: imports)(_.add_edge(_, name))
+
+ val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
+ val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
+ val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
+
+ graph2.map_node(name, _ => syntax)
+ })
+
+ def loaded_files: List[(String, List[Path])] =
+ {
+ names.map(_.theory) zip
+ Par_List.map((e: () => List[Path]) => e(),
+ names.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)).
+ filter(session_base.loaded_theories.defined(_))
+
+ base_theories.map(theory => session_base.known.theories(theory).path) :::
+ base_theories.flatMap(session_base.known.loaded_files(_))
+ }
+
+ lazy val overall_syntax: Outer_Syntax =
+ Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
+
+ override def toString: String = entries.toString
+ }
+
+ private def show_path(names: List[Document.Node.Name]): String =
+ names.map(name => quote(name.theory)).mkString(" via ")
+
+ private def cycle_msg(names: List[Document.Node.Name]): String =
+ "Cyclic dependency of " + show_path(names)
+
+ private def required_by(initiators: List[Document.Node.Name]): String =
+ if (initiators.isEmpty) ""
+ else "\n(required by " + show_path(initiators.reverse) + ")"
+
+ private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+ thy: (Document.Node.Name, Position.T)): Dependencies =
+ {
+ val (name, pos) = thy
+
+ def message: String =
+ "The error(s) above occurred for theory " + quote(name.theory) +
+ required_by(initiators) + Position.here(pos)
+
+ val required1 = required + name
+ if (required.seen(name)) required
+ else if (session_base.loaded_theory(name)) required1
+ else {
+ try {
+ if (initiators.contains(name)) error(cycle_msg(initiators))
+ val header =
+ try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
+ catch { case ERROR(msg) => cat_error(msg, message) }
+ Document.Node.Entry(name, header) ::
+ require_thys(name :: initiators, required1, header.imports)
+ }
+ catch {
+ case e: Throwable =>
+ Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+ }
+ }
+ }
+
+ private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+ thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+ (required /: thys)(require_thy(initiators, _, _))
+
+ def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+ require_thys(Nil, Dependencies.empty, thys)
}
--- a/src/Pure/Thy/sessions.scala Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Oct 31 15:55:50 2017 +0100
@@ -222,7 +222,7 @@
}
val thy_deps =
- resources.thy_info.dependencies(
+ resources.dependencies(
for { (_, thys) <- info.theories; (thy, pos) <- thys }
yield (resources.import_name(info.name, info.dir.implode, thy), pos))
--- a/src/Pure/Thy/thy_info.scala Tue Oct 31 15:36:50 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-/* Title: Pure/Thy/thy_info.scala
- Author: Makarius
-
-Theory and file dependencies.
-*/
-
-package isabelle
-
-
-class Thy_Info(resources: Resources)
-{
- /* messages */
-
- private def show_path(names: List[Document.Node.Name]): String =
- names.map(name => quote(name.theory)).mkString(" via ")
-
- private def cycle_msg(names: List[Document.Node.Name]): String =
- "Cyclic dependency of " + show_path(names)
-
- private def required_by(initiators: List[Document.Node.Name]): String =
- if (initiators.isEmpty) ""
- else "\n(required by " + show_path(initiators.reverse) + ")"
-
-
- /* dependencies */
-
- object Dependencies
- {
- val empty = new Dependencies(Nil, Set.empty)
- }
-
- final class Dependencies private(
- rev_entries: List[Document.Node.Entry],
- val seen: Set[Document.Node.Name])
- {
- def :: (entry: Document.Node.Entry): Dependencies =
- new Dependencies(entry :: rev_entries, seen)
-
- def + (name: Document.Node.Name): Dependencies =
- 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 errors: List[String] = entries.flatMap(_.header.errors)
-
- lazy val loaded_theories: Graph[String, Outer_Syntax] =
- (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
- val name = entry.name.theory
- val imports = entry.header.imports.map(p => p._1.theory)
-
- val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
- val graph2 = (graph1 /: imports)(_.add_edge(_, name))
-
- val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
- val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
- val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
-
- graph2.map_node(name, _ => syntax)
- })
-
- def loaded_files: List[(String, List[Path])] =
- {
- names.map(_.theory) zip
- Par_List.map((e: () => List[Path]) => e(),
- names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
- }
-
- def imported_files: List[Path] =
- {
- val base = resources.session_base
- val base_theories =
- loaded_theories.all_preds(names.map(_.theory)).
- filter(base.loaded_theories.defined(_))
-
- base_theories.map(theory => base.known.theories(theory).path) :::
- base_theories.flatMap(base.known.loaded_files(_))
- }
-
- lazy val overall_syntax: Outer_Syntax =
- Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
-
- override def toString: String = entries.toString
- }
-
- private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
- thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- (required /: thys)(require_thy(initiators, _, _))
-
- private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
- thy: (Document.Node.Name, Position.T)): Dependencies =
- {
- val (name, pos) = thy
-
- def message: String =
- "The error(s) above occurred for theory " + quote(name.theory) +
- required_by(initiators) + Position.here(pos)
-
- val required1 = required + name
- if (required.seen(name)) required
- else if (resources.session_base.loaded_theory(name)) required1
- else {
- try {
- if (initiators.contains(name)) error(cycle_msg(initiators))
- val header =
- try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
- catch { case ERROR(msg) => cat_error(msg, message) }
- Document.Node.Entry(name, header) ::
- require_thys(name :: initiators, required1, header.imports)
- }
- catch {
- case e: Throwable =>
- Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
- }
- }
- }
-
- def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- require_thys(Nil, Dependencies.empty, thys)
-}
--- a/src/Pure/build-jars Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Pure/build-jars Tue Oct 31 15:55:50 2017 +0100
@@ -129,7 +129,6 @@
Thy/present.scala
Thy/sessions.scala
Thy/thy_header.scala
- Thy/thy_info.scala
Thy/thy_syntax.scala
Tools/bibtex.scala
Tools/build.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Oct 31 15:55:50 2017 +0100
@@ -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).names
+ val thy_files = dependencies(thys).names
/* auxiliary files */
--- a/src/Tools/jEdit/src/document_model.scala Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Oct 31 15:55:50 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.thy_info.dependencies(imports).names.toSet
+ val retain = PIDE.resources.dependencies(imports).names.toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit
--- a/src/Tools/jEdit/src/plugin.scala Tue Oct 31 15:36:50 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Oct 31 15:55:50 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.thy_info.dependencies(thys).names
+ val thy_files = resources.dependencies(thys).names
val aux_files =
if (options.bool("jedit_auto_resolve")) {