src/Pure/Tools/build.scala
changeset 64854 f5aa712e6250
parent 64839 842163abfc0d
child 64855 8fcc23e8e1d9
     1.1 --- a/src/Pure/Tools/build.scala	Mon Jan 09 19:34:16 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 09 20:26:59 2017 +0100
     1.3 @@ -98,7 +98,12 @@
     1.4    object Session_Content
     1.5    {
     1.6      def empty: Session_Content =
     1.7 -      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty, Nil, Graph_Display.empty_graph)
     1.8 +      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
     1.9 +        Nil, Graph_Display.empty_graph)
    1.10 +
    1.11 +    def bootstrap: Session_Content =
    1.12 +      Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
    1.13 +        Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
    1.14    }
    1.15  
    1.16    sealed case class Session_Content(
    1.17 @@ -128,15 +133,12 @@
    1.18            if (progress.stopped) throw Exn.Interrupt()
    1.19  
    1.20            try {
    1.21 -            val (loaded_theories0, known_theories0, syntax0) =
    1.22 -              info.parent.map(deps(_)) match {
    1.23 -                case None =>
    1.24 -                  (Set.empty[String], Map.empty[String, Document.Node.Name],
    1.25 -                    Thy_Header.bootstrap_syntax)
    1.26 -                case Some(parent) =>
    1.27 -                  (parent.loaded_theories, parent.known_theories, parent.syntax)
    1.28 +            val base =
    1.29 +              info.parent match {
    1.30 +                case None => Session_Content.bootstrap
    1.31 +                case Some(parent) => deps(parent)
    1.32                }
    1.33 -            val resources = new Resources(loaded_theories0, known_theories0, syntax0)
    1.34 +            val resources = new Resources(base)
    1.35  
    1.36              if (verbose || list_files) {
    1.37                val groups =
    1.38 @@ -163,7 +165,7 @@
    1.39              }
    1.40  
    1.41              val known_theories =
    1.42 -              (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
    1.43 +              (base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    1.44                  val name = dep.name
    1.45                  known.get(name.theory) match {
    1.46                    case Some(name1) if name != name1 =>
    1.47 @@ -201,7 +203,7 @@
    1.48              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    1.49  
    1.50              val session_graph =
    1.51 -              Present.session_graph(info.parent getOrElse "", loaded_theories0, thy_deps.deps)
    1.52 +              Present.session_graph(info.parent getOrElse "", base.loaded_theories, thy_deps.deps)
    1.53  
    1.54              val content =
    1.55                Session_Content(loaded_theories, known_theories, keywords, syntax,