src/Pure/Thy/sessions.scala
changeset 69010 b6aad6338488
parent 69009 4861973145e8
child 69014 a2c042364efc
equal deleted inserted replaced
69009:4861973145e8 69010:b6aad6338488
   194     def get(name: String): Option[Base] = session_bases.get(name)
   194     def get(name: String): Option[Base] = session_bases.get(name)
   195 
   195 
   196     def imported_sources(name: String): List[SHA1.Digest] =
   196     def imported_sources(name: String): List[SHA1.Digest] =
   197       session_bases(name).imported_sources.map(_._2)
   197       session_bases(name).imported_sources.map(_._2)
   198 
   198 
   199     def used_theories_conditions(progress: Progress = No_Progress): List[String] =
   199     def used_theories_conditions(warning: String => Unit = _ => ()): List[String] =
   200       for {
   200       for {
   201         session_name <- sessions_structure.build_topological_order
   201         session_name <- sessions_structure.build_topological_order
   202         (options, name) <- session_bases(session_name).used_theories
   202         (options, name) <- session_bases(session_name).used_theories
   203         if {
   203         if {
   204           val conditions =
   204           val conditions =
   205             space_explode(',', options.string("condition")).
   205             space_explode(',', options.string("condition")).
   206               filter(cond => Isabelle_System.getenv(cond) == "")
   206               filter(cond => Isabelle_System.getenv(cond) == "")
   207           if (conditions.isEmpty) true
   207           if (conditions.isEmpty) true
   208           else {
   208           else {
   209             progress.warning(
   209             warning("Skipping theory " + name + "  (condition " + conditions.mkString(" ") + ")")
   210               "Skipping theory " + name + "  (condition " + conditions.mkString(" ") + ")")
       
   211             false
   210             false
   212           }
   211           }
   213         }
   212         }
   214       } yield name.theory
   213       } yield name.theory
   215 
   214