1.1 --- a/src/Pure/System/build.scala	Tue Aug 14 12:21:32 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Tue Aug 14 12:26:02 2012 +0200
     1.3 @@ -145,6 +145,8 @@
     1.4  
     1.5      def topological_order: List[(String, Session_Info)] =
     1.6        graph.topological_order.map(name => (name, apply(name)))
     1.7 +
     1.8 +    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
     1.9    }
    1.10  
    1.11  
    1.12 @@ -309,7 +311,15 @@
    1.13    sealed case class Session_Content(
    1.14      loaded_theories: Set[String],
    1.15      syntax: Outer_Syntax,
    1.16 -    sources: List[(Path, SHA1.Digest)])
    1.17 +    sources: List[(Path, SHA1.Digest)],
    1.18 +    errors: List[String])
    1.19 +  {
    1.20 +    def check_errors: Session_Content =
    1.21 +    {
    1.22 +      if (errors.isEmpty) this
    1.23 +      else error(cat_lines(errors))
    1.24 +    }
    1.25 +  }
    1.26  
    1.27    sealed case class Deps(deps: Map[String, Session_Content])
    1.28    {
    1.29 @@ -321,16 +331,19 @@
    1.30    def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
    1.31      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    1.32        { case (deps, (name, info)) =>
    1.33 -          val (preloaded, parent_syntax) =
    1.34 +          val (preloaded, parent_syntax, parent_errors) =
    1.35              info.parent match {
    1.36 -              case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax)
    1.37 +              case Some(parent_name) =>
    1.38 +                val parent = deps(parent_name)
    1.39 +                (parent.loaded_theories, parent.syntax, parent.errors)
    1.40                case None =>
    1.41 -                (Set.empty[String],
    1.42 +                val init_syntax =
    1.43                    Outer_Syntax.init() +
    1.44                      // FIXME avoid hardwired stuff!?
    1.45                      ("theory", Keyword.THY_BEGIN) +
    1.46                      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
    1.47 -                    ("thus", Keyword.PRF_ASM_GOAL, "then show"))
    1.48 +                    ("thus", Keyword.PRF_ASM_GOAL, "then show")
    1.49 +                (Set.empty[String], init_syntax, Nil)
    1.50              }
    1.51            val thy_info = new Thy_Info(new Thy_Load(preloaded))
    1.52  
    1.53 @@ -362,8 +375,9 @@
    1.54                  error(msg + "\nThe error(s) above occurred in session " +
    1.55                    quote(name) + Position.str_of(info.pos))
    1.56              }
    1.57 +          val errors = parent_errors ::: thy_deps.map(d => d._2.errors).flatten
    1.58  
    1.59 -          deps + (name -> Session_Content(loaded_theories, syntax, sources))
    1.60 +          deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
    1.61        }))
    1.62  
    1.63    def session_content(dirs: List[Path], session: String): Session_Content =
    1.64 @@ -373,7 +387,8 @@
    1.65      dependencies(false, tree)(session)
    1.66    }
    1.67  
    1.68 -  def outer_syntax(session: String): Outer_Syntax = session_content(Nil, session).syntax
    1.69 +  def outer_syntax(session: String): Outer_Syntax =
    1.70 +    session_content(Nil, session).check_errors.syntax
    1.71  
    1.72  
    1.73    /* jobs */

     2.1 --- a/src/Pure/System/session.scala	Tue Aug 14 12:21:32 2012 +0200
     2.2 +++ b/src/Pure/System/session.scala	Tue Aug 14 12:26:02 2012 +0200
     2.3 @@ -382,7 +382,7 @@
     2.4              phase = Session.Startup
     2.5  
     2.6              // FIXME static init in main constructor
     2.7 -            val content = Build.session_content(dirs, name)
     2.8 +            val content = Build.session_content(dirs, name).check_errors
     2.9              thy_load.register_thys(content.loaded_theories)
    2.10              base_syntax = content.syntax
    2.11