# HG changeset patch
# User wenzelm
# Date 1537215072 -7200
# Node ID 8745ca1e7e9309000edef002297a078bc2ae41d4
# Parent  e2d573447efdfe091e5df6c57b07d807e040355e# Parent  b6aad633848882c25a39d556376f54b92ad53c98
merged

diff -r e2d573447efd -r 8745ca1e7e93 src/Pure/PIDE/resources.scala
--- 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)
 }
diff -r e2d573447efd -r 8745ca1e7e93 src/Pure/Thy/sessions.scala
--- 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),
diff -r e2d573447efd -r 8745ca1e7e93 src/Pure/Tools/dump.scala
--- 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 */