avoid duplicate invocation of expensive Sessions.deps on full_sessions;
authorwenzelm
Wed Nov 01 16:31:27 2017 +0100 (19 months ago)
changeset 66974b14c24b31f45
parent 66973 829c3133c4ca
child 66975 ca73d44d51aa
avoid duplicate invocation of expensive Sessions.deps on full_sessions;
tuned;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 01 15:32:07 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 16:31:27 2017 +0100
     1.3 @@ -325,42 +325,48 @@
     1.4  
     1.5    /* base info */
     1.6  
     1.7 +  sealed case class Base_Info(
     1.8 +    session: String,
     1.9 +    sessions: T,
    1.10 +    deps: Deps,
    1.11 +    base: Base,
    1.12 +    infos: List[Info])
    1.13 +  {
    1.14 +    def errors: List[String] = deps.errors
    1.15 +    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.16 +  }
    1.17 +
    1.18    def session_base_info(
    1.19      options: Options,
    1.20      session: String,
    1.21      dirs: List[Path] = Nil,
    1.22 -    infos: List[Info] = Nil,
    1.23      all_known: Boolean = false,
    1.24      required_session: Boolean = false): Base_Info =
    1.25    {
    1.26 -    val full_sessions = load(options, dirs = dirs, infos = infos)
    1.27 +    val full_sessions = load(options, dirs = dirs)
    1.28      val global_theories = full_sessions.global_theories
    1.29 -    val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.30  
    1.31 -    val sessions: T = if (all_known) full_sessions else selected_sessions
    1.32 -    val deps = Sessions.deps(sessions, global_theories)
    1.33 -    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.34 +    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
    1.35 +    val info = selected_sessions(session)
    1.36  
    1.37 -    val other_session: Option[(String, List[Info])] =
    1.38 -      if (required_session && !is_pure(session)) {
    1.39 -        val info = sessions(session)
    1.40 +    val (session1, infos1) =
    1.41 +      if (required_session && info.parent.isDefined) {
    1.42 +        val deps = Sessions.deps(selected_sessions, global_theories)
    1.43 +        val base = deps(session)
    1.44  
    1.45 -        val parent_loaded =
    1.46 -          info.parent match {
    1.47 -            case Some(parent) => deps(parent).loaded_theories.defined(_)
    1.48 -            case None => (_: String) => false
    1.49 -          }
    1.50 -        val imported_theories =
    1.51 +        val parent_loaded = deps(info.parent.get).loaded_theories.defined(_)
    1.52 +
    1.53 +        val required_theories =
    1.54            for {
    1.55              thy <- base.loaded_theories.keys
    1.56              if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    1.57            }
    1.58 -          yield (List.empty[Options.Spec], List(((thy, Position.none), false)))
    1.59 +          yield thy
    1.60  
    1.61 -        if (imported_theories.isEmpty) info.parent.map((_, Nil))
    1.62 +        if (required_theories.isEmpty) (info.parent.get, Nil)
    1.63          else {
    1.64            val other_name = info.name + "(imports)"
    1.65 -          Some((other_name,
    1.66 +          (other_name,
    1.67              List(
    1.68                make_info(info.options,
    1.69                  dir_selected = false,
    1.70 @@ -372,30 +378,25 @@
    1.71                    groups = info.groups,
    1.72                    path = ".",
    1.73                    parent = info.parent,
    1.74 -                  description = "All required theory imports from other sessions",
    1.75 +                  description = "Required theory imports from other sessions",
    1.76                    options = Nil,
    1.77                    imports = info.imports,
    1.78 -                  theories = imported_theories,
    1.79 -                  document_files = Nil)))))
    1.80 +                  theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
    1.81 +                  document_files = Nil))))
    1.82          }
    1.83        }
    1.84 -      else None
    1.85 +      else (session, Nil)
    1.86  
    1.87 -    other_session match {
    1.88 -      case None => new Base_Info(session, sessions, deps, base, infos)
    1.89 -      case Some((other_name, more_infos)) =>
    1.90 -        session_base_info(options, other_name,
    1.91 -          dirs = dirs, infos = more_infos ::: infos, all_known = all_known)
    1.92 -    }
    1.93 -  }
    1.94 +    val full_sessions1 =
    1.95 +      if (infos1.isEmpty) full_sessions
    1.96 +      else load(options, dirs = dirs, infos = infos1)
    1.97 +    val selected_sessions1 = full_sessions1.selection(Selection(sessions = List(session1)))._2
    1.98  
    1.99 -  final class Base_Info private [Sessions](
   1.100 -    val session: String, val sessions: T, val deps: Deps, val base: Base, val infos: List[Info])
   1.101 -  {
   1.102 -    override def toString: String = session
   1.103 +    val sessions1 = if (all_known) full_sessions1 else selected_sessions1
   1.104 +    val deps1 = Sessions.deps(sessions1, global_theories)
   1.105 +    val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
   1.106  
   1.107 -    def errors: List[String] = deps.errors
   1.108 -    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   1.109 +    Base_Info(session1, sessions1, deps1, base1, infos1)
   1.110    }
   1.111  
   1.112