src/Pure/Tools/build.scala
changeset 64856 5e9bf964510a
parent 64855 8fcc23e8e1d9
child 64909 8007f10195af
     1.1 --- a/src/Pure/Tools/build.scala	Mon Jan 09 20:31:00 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 09 20:47:45 2017 +0100
     1.3 @@ -95,29 +95,10 @@
     1.4  
     1.5    /* source dependencies and static content */
     1.6  
     1.7 -  object Session_Content
     1.8 -  {
     1.9 -    val empty: Session_Content =
    1.10 -      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
    1.11 -        Nil, Graph_Display.empty_graph)
    1.12 -
    1.13 -    lazy val bootstrap: Session_Content =
    1.14 -      Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
    1.15 -        Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
    1.16 -  }
    1.17 -
    1.18 -  sealed case class Session_Content(
    1.19 -    loaded_theories: Set[String],
    1.20 -    known_theories: Map[String, Document.Node.Name],
    1.21 -    keywords: Thy_Header.Keywords,
    1.22 -    syntax: Outer_Syntax,
    1.23 -    sources: List[(Path, SHA1.Digest)],
    1.24 -    session_graph: Graph_Display.Graph)
    1.25 -
    1.26 -  sealed case class Deps(deps: Map[String, Session_Content])
    1.27 +  sealed case class Deps(deps: Map[String, Sessions.Base])
    1.28    {
    1.29      def is_empty: Boolean = deps.isEmpty
    1.30 -    def apply(name: String): Session_Content = deps(name)
    1.31 +    def apply(name: String): Sessions.Base = deps(name)
    1.32      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    1.33    }
    1.34  
    1.35 @@ -128,17 +109,17 @@
    1.36        list_files: Boolean = false,
    1.37        check_keywords: Set[String] = Set.empty,
    1.38        tree: Sessions.Tree): Deps =
    1.39 -    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    1.40 +    Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
    1.41        { case (deps, (name, info)) =>
    1.42            if (progress.stopped) throw Exn.Interrupt()
    1.43  
    1.44            try {
    1.45 -            val base =
    1.46 -              info.parent match {
    1.47 -                case None => Session_Content.bootstrap
    1.48 -                case Some(parent) => deps(parent)
    1.49 -              }
    1.50 -            val resources = new Resources(base)
    1.51 +            val resources =
    1.52 +              new Resources(
    1.53 +                info.parent match {
    1.54 +                  case None => Sessions.Base.bootstrap
    1.55 +                  case Some(parent) => deps(parent)
    1.56 +                })
    1.57  
    1.58              if (verbose || list_files) {
    1.59                val groups =
    1.60 @@ -165,7 +146,7 @@
    1.61              }
    1.62  
    1.63              val known_theories =
    1.64 -              (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    1.65 +              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    1.66                  val name = dep.name
    1.67                  known.get(name.theory) match {
    1.68                    case Some(name1) if name != name1 =>
    1.69 @@ -203,12 +184,13 @@
    1.70              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    1.71  
    1.72              val session_graph =
    1.73 -              Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
    1.74 +              Present.session_graph(info.parent getOrElse "",
    1.75 +                resources.base.loaded_theories, thy_deps.deps)
    1.76  
    1.77 -            val content =
    1.78 -              Session_Content(loaded_theories, known_theories, keywords, syntax,
    1.79 -                sources, session_graph)
    1.80 -            deps + (name -> content)
    1.81 +            val base =
    1.82 +              Sessions.Base(
    1.83 +                loaded_theories, known_theories, keywords, syntax, sources, session_graph)
    1.84 +            deps + (name -> base)
    1.85            }
    1.86            catch {
    1.87              case ERROR(msg) =>
    1.88 @@ -227,17 +209,17 @@
    1.89      dependencies(inlined_files = inlined_files, tree = tree)
    1.90    }
    1.91  
    1.92 -  def session_content(
    1.93 +  def session_base(
    1.94      options: Options,
    1.95      inlined_files: Boolean,
    1.96      dirs: List[Path],
    1.97 -    session: String): Session_Content =
    1.98 +    session: String): Sessions.Base =
    1.99    {
   1.100      session_dependencies(options, inlined_files, dirs, List(session))(session)
   1.101    }
   1.102  
   1.103    def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
   1.104 -    session_content(options, false, dirs, session).syntax
   1.105 +    session_base(options, false, dirs, session).syntax
   1.106  
   1.107  
   1.108    /* jobs */