allow to augment session context via explicit session infos;
authorwenzelm
Tue Oct 31 21:50:09 2017 +0100 (18 months ago)
changeset 669689991671c98aa
parent 66967 e365c91c72a9
child 66969 39077839947e
allow to augment session context via explicit session infos;
more compact required_session interface;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 20:57:44 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 21:50:09 2017 +0100
     1.3 @@ -329,10 +329,12 @@
     1.4      options: Options,
     1.5      session: String,
     1.6      dirs: List[Path] = Nil,
     1.7 +    infos: List[Info] = Nil,
     1.8      inlined_files: Boolean = false,
     1.9 -    all_known: Boolean = false): Base_Info =
    1.10 +    all_known: Boolean = false,
    1.11 +    required_session: Boolean = false): Base_Info =
    1.12    {
    1.13 -    val full_sessions = load(options, dirs = dirs)
    1.14 +    val full_sessions = load(options, dirs = dirs, infos = infos)
    1.15      val global_theories = full_sessions.global_theories
    1.16      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.17  
    1.18 @@ -340,52 +342,61 @@
    1.19      val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    1.20      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.21  
    1.22 -    new Base_Info(session, sessions, deps, base)
    1.23 +    val other_session: Option[(String, List[Info])] =
    1.24 +      if (required_session && !is_pure(session)) {
    1.25 +        val info = sessions(session)
    1.26 +
    1.27 +        val parent_loaded =
    1.28 +          info.parent match {
    1.29 +            case Some(parent) => deps(parent).loaded_theories.defined(_)
    1.30 +            case None => (_: String) => false
    1.31 +          }
    1.32 +        val imported_theories =
    1.33 +          for {
    1.34 +            thy <- base.loaded_theories.keys
    1.35 +            if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    1.36 +          }
    1.37 +          yield (List.empty[Options.Spec], List(((thy, Position.none), false)))
    1.38 +
    1.39 +        if (imported_theories.isEmpty) info.parent.map((_, Nil))
    1.40 +        else {
    1.41 +          val other_name = info.name + "(imports)"
    1.42 +          Some((other_name,
    1.43 +            List(
    1.44 +              make_info(info.options,
    1.45 +                dir_selected = false,
    1.46 +                dir = info.dir,
    1.47 +                chapter = info.chapter,
    1.48 +                Session_Entry(
    1.49 +                  pos = info.pos,
    1.50 +                  name = other_name,
    1.51 +                  groups = info.groups,
    1.52 +                  path = ".",
    1.53 +                  parent = info.parent,
    1.54 +                  description = "All required theory imports from other sessions",
    1.55 +                  options = Nil,
    1.56 +                  imports = info.imports,
    1.57 +                  theories = imported_theories,
    1.58 +                  document_files = Nil)))))
    1.59 +        }
    1.60 +      }
    1.61 +      else None
    1.62 +
    1.63 +    other_session match {
    1.64 +      case None => new Base_Info(session, sessions, deps, base, infos)
    1.65 +      case Some((other_name, more_infos)) =>
    1.66 +        session_base_info(options, other_name, dirs = dirs, infos = more_infos ::: infos,
    1.67 +          inlined_files = inlined_files, all_known = all_known)
    1.68 +    }
    1.69    }
    1.70  
    1.71    final class Base_Info private [Sessions](
    1.72 -    val session: String, val sessions: T, val deps: Deps, val base: Base)
    1.73 +    val session: String, val sessions: T, val deps: Deps, val base: Base, val infos: List[Info])
    1.74    {
    1.75      override def toString: String = session
    1.76  
    1.77      def errors: List[String] = deps.errors
    1.78      def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.79 -
    1.80 -    def imported_session: Option[Info] =
    1.81 -    {
    1.82 -      val info = sessions(session)
    1.83 -
    1.84 -      val parent_loaded =
    1.85 -        info.parent match {
    1.86 -          case Some(parent) => deps(parent).loaded_theories.defined(_)
    1.87 -          case None => (_: String) => false
    1.88 -        }
    1.89 -      val imported_theories =
    1.90 -        for {
    1.91 -          thy <- base.loaded_theories.keys
    1.92 -          if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    1.93 -        }
    1.94 -        yield (List.empty[Options.Spec], List(((thy, Position.none), false)))
    1.95 -
    1.96 -      if (imported_theories.isEmpty) None
    1.97 -      else
    1.98 -        Some(
    1.99 -          make_info(info.options,
   1.100 -            dir_selected = false,
   1.101 -            dir = info.dir,
   1.102 -            chapter = info.chapter,
   1.103 -            Session_Entry(
   1.104 -              pos = info.pos,
   1.105 -              name = info.name + "(base)",
   1.106 -              groups = info.groups,
   1.107 -              path = ".",
   1.108 -              parent = info.parent,
   1.109 -              description = "All required theories from other session imports",
   1.110 -              options = Nil,
   1.111 -              imports = info.imports,
   1.112 -              theories = imported_theories,
   1.113 -              document_files = Nil)))
   1.114 -    }
   1.115    }
   1.116  
   1.117  
   1.118 @@ -759,7 +770,10 @@
   1.119      (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   1.120    }
   1.121  
   1.122 -  def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
   1.123 +  def load(options: Options,
   1.124 +    dirs: List[Path] = Nil,
   1.125 +    select_dirs: List[Path] = Nil,
   1.126 +    infos: List[Info] = Nil): T =
   1.127    {
   1.128      def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
   1.129        load_root(select, dir) ::: load_roots(select, dir)
   1.130 @@ -803,7 +817,7 @@
   1.131          }
   1.132        }).toList.map(_._2)
   1.133  
   1.134 -    make(unique_roots.flatMap(p => read_root(options, p._1, p._2)))
   1.135 +    make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
   1.136    }
   1.137  
   1.138  
     2.1 --- a/src/Pure/Tools/build.scala	Tue Oct 31 20:57:44 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 31 21:50:09 2017 +0100
     2.3 @@ -354,6 +354,7 @@
     2.4      clean_build: Boolean = false,
     2.5      dirs: List[Path] = Nil,
     2.6      select_dirs: List[Path] = Nil,
     2.7 +    infos: List[Sessions.Info] = Nil,
     2.8      numa_shuffling: Boolean = false,
     2.9      max_jobs: Int = 1,
    2.10      list_files: Boolean = false,
    2.11 @@ -381,7 +382,7 @@
    2.12      /* session selection and dependencies */
    2.13  
    2.14      val full_sessions =
    2.15 -      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs)
    2.16 +      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
    2.17  
    2.18      def sources_stamp(deps: Sessions.Deps, name: String): String =
    2.19      {