# HG changeset patch
# User wenzelm
# Date 1537213814 -7200
# Node ID d55783ea6cf6fc0aa6a874626ccfad46c13f4c7b
# Parent  2ac19d346b83a651cf301cd9e815c92b18f2a27a
more detailed session dependencies, with conditions for theories;

diff -r 2ac19d346b83 -r d55783ea6cf6 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Sep 17 20:30:53 2018 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Sep 17 21:50:14 2018 +0200
@@ -223,12 +223,25 @@
 
   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],
-      progress: Progress = No_Progress): Dependencies =
-    Dependencies.empty.require_thys(thys, progress = progress)
+      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: Dependencies = 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 ")
@@ -241,17 +254,17 @@
       else "\n(required by " + show_path(initiators.reverse) + ")"
   }
 
-  final class Dependencies private(
+  final class Dependencies[A] private(
     rev_entries: List[Document.Node.Entry],
-    seen: Set[Document.Node.Name])
+    seen: Map[Document.Node.Name, A])
   {
-    private def cons(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(
+    def require_thy(adjunct: A,
       thy: (Document.Node.Name, Position.T),
       initiators: List[Document.Node.Name] = Nil,
-      progress: Progress = No_Progress): Dependencies =
+      progress: Progress = No_Progress): Dependencies[A] =
     {
       val (name, pos) = thy
 
@@ -259,9 +272,9 @@
         "The error(s) above occurred for theory " + quote(name.theory) +
           Dependencies.required_by(initiators) + Position.here(pos)
 
-      if (seen(name)) this
+      if (seen.isDefinedAt(name)) this
       else {
-        val dependencies1 = new Dependencies(rev_entries, seen + name)
+        val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
         if (session_base.loaded_theory(name)) dependencies1
         else {
           try {
@@ -272,8 +285,8 @@
               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(
-              header.imports, initiators = name :: initiators, progress = progress).cons(entry)
+            dependencies1.require_thys(adjunct, header.imports,
+              initiators = name :: initiators, progress = progress).cons(entry)
           }
           catch {
             case e: Throwable =>
@@ -283,18 +296,20 @@
       }
     }
 
-    def require_thys(
+    def require_thys(adjunct: A,
         thys: List[(Document.Node.Name, Position.T)],
         progress: Progress = No_Progress,
-        initiators: List[Document.Node.Name] = Nil): Dependencies =
-      (this /: thys)(_.require_thy(_, progress = progress, initiators = initiators))
+        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))
diff -r 2ac19d346b83 -r d55783ea6cf6 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),
diff -r 2ac19d346b83 -r d55783ea6cf6 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 17 20:30:53 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 17 21:50:14 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)
 
 
     /* dump aspects asynchronously */