--- a/src/Pure/PIDE/resources.scala Mon Sep 17 19:21:39 2018 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Sep 17 22:11:12 2018 +0200
@@ -221,27 +221,95 @@
/* theory and file dependencies */
+ def dependencies(
+ thys: List[(Document.Node.Name, Position.T)],
+ progress: Progress = No_Progress): Dependencies[Unit] =
+ Dependencies.empty[Unit].require_thys((), thys, progress = progress)
+
+ def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
+ : Dependencies[Options] =
+ {
+ val qualifier = info.name
+ val dir = info.dir.implode
+
+ (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
+ dependencies.require_thys(options,
+ for { (thy, pos) <- thys } yield (import_name(qualifier, dir, thy), pos),
+ progress = progress)
+ })
+ }
+
object Dependencies
{
- val empty = new Dependencies(Nil, Set.empty)
+ def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty)
+
+ 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) + ")"
}
- final class Dependencies private(
+ final class Dependencies[A] private(
rev_entries: List[Document.Node.Entry],
- val seen: Set[Document.Node.Name])
+ seen: Map[Document.Node.Name, A])
{
- def :: (entry: Document.Node.Entry): Dependencies =
- new Dependencies(entry :: rev_entries, seen)
+ private def cons(entry: Document.Node.Entry): Dependencies[A] =
+ new Dependencies[A](entry :: rev_entries, seen)
+
+ def require_thy(adjunct: A,
+ thy: (Document.Node.Name, Position.T),
+ initiators: List[Document.Node.Name] = Nil,
+ progress: Progress = No_Progress): Dependencies[A] =
+ {
+ val (name, pos) = thy
+
+ def message: String =
+ "The error(s) above occurred for theory " + quote(name.theory) +
+ Dependencies.required_by(initiators) + Position.here(pos)
+
+ if (seen.isDefinedAt(name)) this
+ else {
+ val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
+ if (session_base.loaded_theory(name)) dependencies1
+ else {
+ try {
+ if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
- def + (name: Document.Node.Name): Dependencies =
- new Dependencies(rev_entries, seen + name)
+ progress.expose_interrupt()
+ val header =
+ try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
+ catch { case ERROR(msg) => cat_error(msg, message) }
+ val entry = Document.Node.Entry(name, header)
+ dependencies1.require_thys(adjunct, header.imports,
+ initiators = name :: initiators, progress = progress).cons(entry)
+ }
+ catch {
+ case e: Throwable =>
+ dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))))
+ }
+ }
+ }
+ }
+
+ def require_thys(adjunct: A,
+ thys: List[(Document.Node.Name, Position.T)],
+ progress: Progress = No_Progress,
+ initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
+ (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
def entries: List[Document.Node.Entry] = rev_entries.reverse
+
def theories: List[Document.Node.Name] = entries.map(_.name)
+ def adjunct_theories: List[(A, Document.Node.Name)] = theories.map(name => (seen(name), name))
def errors: List[String] = entries.flatMap(_.header.errors)
- def check_errors: Dependencies =
+ def check_errors: Dependencies[A] =
errors match {
case Nil => this
case errs => error(cat_lines(errs))
@@ -284,61 +352,4 @@
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(
- progress: Progress,
- initiators: List[Document.Node.Name],
- dependencies: 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)
-
- if (dependencies.seen(name)) dependencies
- else {
- val dependencies1 = dependencies + name
- if (session_base.loaded_theory(name)) dependencies1
- else {
- try {
- if (initiators.contains(name)) error(cycle_msg(initiators))
-
- progress.expose_interrupt()
- 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(progress, name :: initiators, dependencies1, header.imports)
- }
- catch {
- case e: Throwable =>
- Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: dependencies1
- }
- }
- }
- }
-
- private def require_thys(
- progress: Progress,
- initiators: List[Document.Node.Name],
- dependencies: Dependencies,
- thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- (dependencies /: thys)(require_thy(progress, initiators, _, _))
-
- def dependencies(
- thys: List[(Document.Node.Name, Position.T)],
- progress: Progress = No_Progress): Dependencies =
- require_thys(progress, Nil, Dependencies.empty, thys)
}
--- a/src/Pure/Thy/sessions.scala Mon Sep 17 19:21:39 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Sep 17 22:11:12 2018 +0200
@@ -149,7 +149,7 @@
doc_names: List[String] = Nil,
global_theories: Map[String, String] = Map.empty,
loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
- used_theories: List[Document.Node.Name] = Nil,
+ used_theories: List[(Options, Document.Node.Name)] = Nil,
known: Known = Known.empty,
overall_syntax: Outer_Syntax = Outer_Syntax.empty,
imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -196,6 +196,22 @@
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
+ def used_theories_conditions(warning: String => Unit = _ => ()): List[String] =
+ for {
+ session_name <- sessions_structure.build_topological_order
+ (options, name) <- session_bases(session_name).used_theories
+ if {
+ val conditions =
+ space_explode(',', options.string("condition")).
+ filter(cond => Isabelle_System.getenv(cond) == "")
+ if (conditions.isEmpty) true
+ else {
+ warning("Skipping theory " + name + " (condition " + conditions.mkString(" ") + ")")
+ false
+ }
+ }
+ } yield name.theory
+
def sources(name: String): List[SHA1.Digest] =
session_bases(name).sources.map(_._2)
@@ -268,10 +284,7 @@
progress.echo("Session " + info.chapter + "/" + info.name + groups)
}
- val dependencies =
- resources.dependencies(
- for { (_, thys) <- info.theories; (thy, pos) <- thys }
- yield (resources.import_name(info.name, info.dir.implode, thy), pos))
+ val dependencies = resources.session_dependencies(info)
val overall_syntax = dependencies.overall_syntax
@@ -353,7 +366,7 @@
doc_names = doc_names,
global_theories = global_theories,
loaded_theories = dependencies.loaded_theories,
- used_theories = dependencies.theories,
+ used_theories = dependencies.adjunct_theories,
known = known,
overall_syntax = overall_syntax,
imported_sources = check_sources(imported_files),
--- a/src/Pure/Tools/dump.scala Mon Sep 17 19:21:39 2018 +0200
+++ b/src/Pure/Tools/dump.scala Mon Sep 17 22:11:12 2018 +0200
@@ -112,9 +112,7 @@
val include_sessions =
deps.sessions_structure.imports_topological_order
- val use_theories =
- deps.sessions_structure.build_topological_order.
- flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
+ val use_theories = deps.used_theories_conditions(progress.echo_warning)
/* dump aspects asynchronously */