actually expose errors of cumulative theory dependencies;
more informative error messages;

--- a/src/Pure/PIDE/document.scala	Thu Nov 21 17:45:37 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 21 17:50:23 2013 +0100
@@ -62,6 +62,9 @@
       errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
+
+      def cat_errors(msg2: String): Header =
+        copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
     }
 
     def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))

--- a/src/Pure/Thy/thy_info.scala	Thu Nov 21 17:45:37 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Thu Nov 21 17:50:23 2013 +0100
@@ -58,6 +58,8 @@
 
     def deps: List[Dep] = rev_deps.reverse
 
+    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
+
     lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
 
     def loaded_theories: Set[String] =
@@ -86,15 +88,15 @@
     if (required.seen(name)) required
     else if (thy_load.loaded_theories(name.theory)) required + name
     else {
-      def err(msg: String): Nothing =
-        cat_error(msg, "The error(s) above occurred while examining theory " +
-          quote(name.theory) + required_by(initiators))
+      def message: String =
+        "The error(s) above occurred while examining theory " +
+          quote(name.theory) + required_by(initiators)
 
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { thy_load.check_thy(name) }
-          catch { case ERROR(msg) => err(msg) }
+          try { thy_load.check_thy(name).cat_errors(message) }
+          catch { case ERROR(msg) => cat_error(msg, message) }
         Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
       }
       catch {

--- a/src/Pure/Tools/build.scala	Thu Nov 21 17:45:37 2013 +0100
+++ b/src/Pure/Tools/build.scala	Thu Nov 21 17:50:23 2013 +0100
@@ -409,65 +409,68 @@
       verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
-          val (preloaded, parent_syntax) =
-            info.parent match {
-              case None =>
-                (Set.empty[String], Outer_Syntax.init())
-              case Some(parent_name) =>
-                val parent = deps(parent_name)
-                (parent.loaded_theories, parent.syntax)
-            }
-          val thy_load = new Thy_Load(preloaded, parent_syntax)
-          val thy_info = new Thy_Info(thy_load)
+          try {
+            val (preloaded, parent_syntax) =
+              info.parent match {
+                case None =>
+                  (Set.empty[String], Outer_Syntax.init())
+                case Some(parent_name) =>
+                  val parent = deps(parent_name)
+                  (parent.loaded_theories, parent.syntax)
+              }
+            val thy_load = new Thy_Load(preloaded, parent_syntax)
+            val thy_info = new Thy_Info(thy_load)
 
-          if (verbose || list_files) {
-            val groups =
-              if (info.groups.isEmpty) ""
-              else info.groups.mkString(" (", " ", ")")
-            progress.echo("Session " + info.chapter + "/" + name + groups)
-          }
+            if (verbose || list_files) {
+              val groups =
+                if (info.groups.isEmpty) ""
+                else info.groups.mkString(" (", " ", ")")
+              progress.echo("Session " + info.chapter + "/" + name + groups)
+            }
 
-          val thy_deps =
-            thy_info.dependencies(
-              info.theories.map(_._2).flatten.
-                map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
+            val thy_deps =
+              thy_info.dependencies(
+                info.theories.map(_._2).flatten.
+                  map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
 
-          val loaded_theories = thy_deps.loaded_theories
-          val keywords = thy_deps.keywords
-          val syntax = thy_deps.syntax
+            thy_deps.errors match {
+              case Nil =>
+              case errs => error(cat_lines(errs))
+            }
 
-          val body_files = if (inlined_files) thy_deps.load_files else Nil
+            val loaded_theories = thy_deps.loaded_theories
+            val keywords = thy_deps.keywords
+            val syntax = thy_deps.syntax
 
-          val all_files =
-            (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
-              info.files.map(file => info.dir + file)).map(_.expand)
+            val body_files = if (inlined_files) thy_deps.load_files else Nil
 
-          if (list_files) {
-            progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
-            for {
-              file <- all_files
-              if file.split_ext._2 == "ML"
-            } {
-              val path = info.dir + file
-              try { Symbol.decode_strict(File.read(path)) }
-              catch {
-                case ERROR(msg) =>
-                  cat_error(msg,
-                    "The error(s) above occurred in session " + quote(name) +
-                      " file " + path.toString)
+            val all_files =
+              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+                info.files.map(file => info.dir + file)).map(_.expand)
+
+            if (list_files) {
+              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
+              for {
+                file <- all_files
+                if file.split_ext._2 == "ML"
+              } {
+                val path = info.dir + file
+                try { Symbol.decode_strict(File.read(path)) }
+                catch {
+                  case ERROR(msg) => cat_error(msg, "The error(s) above occurred in file " + path)
+                }
               }
             }
-          }
+
+            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
 
-          val sources =
-            try { all_files.map(p => (p, SHA1.digest(p.file))) }
-            catch {
-              case ERROR(msg) =>
-                error(msg + "\nThe error(s) above occurred in session " +
-                  quote(name) + Position.here(info.pos))
-            }
-
-          deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
+            deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
+          }
+          catch {
+            case ERROR(msg) =>
+              cat_error(msg, "The error(s) above occurred in session " +
+                quote(name) + Position.here(info.pos))
+          }
       }))
 
   def session_dependencies(