src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Mon Sep 17 20:30:53 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 17 21:50:14 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,23 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
+    def used_theories_conditions(progress: Progress = No_Progress): 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 {
+            progress.echo(
+              "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 +285,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 +367,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),