equal
deleted
inserted
replaced
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 |