# HG changeset patch
# User wenzelm
# Date 1361990356 -3600
# Node ID d9f3d91208afc666d802e61343615b7b8c977614
# Parent  77e71d54efda20adecb7c6723eac8cd5320c046b
eliminated pointless re-ified errors;

diff -r 77e71d54efda -r d9f3d91208af src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 27 17:44:08 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 27 19:39:16 2013 +0100
@@ -368,15 +368,7 @@
   sealed case class Session_Content(
     loaded_theories: Set[String],
     syntax: Outer_Syntax,
-    sources: List[(Path, SHA1.Digest)],
-    errors: List[String])
-  {
-    def check_errors: Session_Content =
-    {
-      if (errors.isEmpty) this
-      else error(cat_lines(errors))
-    }
-  }
+    sources: List[(Path, SHA1.Digest)])
 
   sealed case class Deps(deps: Map[String, Session_Content])
   {
@@ -389,13 +381,13 @@
       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, parent_errors) =
+          val (preloaded, parent_syntax) =
             info.parent match {
               case None =>
-                (Set.empty[String], Outer_Syntax.init_pure(), Nil)
+                (Set.empty[String], Outer_Syntax.init_pure())
               case Some(parent_name) =>
                 val parent = deps(parent_name)
-                (parent.loaded_theories, parent.syntax, parent.errors)
+                (parent.loaded_theories, parent.syntax)
             }
           val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
 
@@ -430,9 +422,8 @@
                 error(msg + "\nThe error(s) above occurred in session " +
                   quote(name) + Position.here(info.pos))
             }
-          val errors = parent_errors
 
-          deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
+          deps + (name -> Session_Content(loaded_theories, syntax, sources))
       }))
 
   def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
@@ -444,7 +435,7 @@
   }
 
   def outer_syntax(session: String): Outer_Syntax =
-    session_content(false, Nil, session).check_errors.syntax
+    session_content(false, Nil, session).syntax
 
 
   /* jobs */
diff -r 77e71d54efda -r d9f3d91208af src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Feb 27 17:44:08 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Feb 27 19:39:16 2013 +0100
@@ -79,7 +79,7 @@
   {
     val dirs = session_dirs()
     val name = session_args().last
-    Build.session_content(inlined_files, dirs, name).check_errors
+    Build.session_content(inlined_files, dirs, name)
   }
 }