store errors in build db;

--- a/src/Pure/Admin/build_log.scala	Fri May 26 11:51:45 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri May 26 15:19:21 2017 +0200
@@ -258,12 +258,11 @@
     def parse_props(text: String): Properties.T =
       xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text))))
 
+    def filter_lines(marker: String): List[String] =
+      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield s
+
     def filter_props(marker: String): List[Properties.T] =
-      for {
-        line <- lines
-        s <- Library.try_unprefix(marker, line)
-        if YXML.detect(s)
-      } yield parse_props(s)
+      for (s <- filter_lines(marker) if YXML.detect(s)) yield parse_props(s)
 
     def find_props(marker: String): Option[Properties.T] =
       find_line(marker) match {
@@ -599,7 +598,8 @@
     session_timing: Properties.T,
     command_timings: List[Properties.T],
     ml_statistics: List[Properties.T],
-    task_statistics: List[Properties.T])
+    task_statistics: List[Properties.T],
+    errors: List[String])
 
   private def parse_session_info(
     log_file: Log_File,
@@ -611,7 +611,8 @@
       session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
       command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
       ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
-      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
+      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil,
+      errors = log_file.filter_lines("\ferror_message = ").map(Library.decode_lines(_)))
   }
 
 

--- a/src/Pure/Thy/sessions.scala	Fri May 26 11:51:45 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri May 26 15:19:21 2017 +0200
@@ -735,8 +735,9 @@
     val command_timings = SQL.Column.bytes("command_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
+    val errors = SQL.Column.bytes("errors")
     val build_log_columns =
-      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
+      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
@@ -814,6 +815,14 @@
 
     /* session info */
 
+    def compress_errors(errors: List[String]): Option[Bytes] =
+      if (errors.isEmpty) None
+      else Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).compress())
+
+    def uncompress_errors(bytes: Bytes): List[String] =
+      if (bytes.isEmpty) Nil
+      else XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress().text))
+
     def write_session_info(
       db: SQL.Database,
       name: String,
@@ -831,10 +840,11 @@
           stmt.bytes(3) = Properties.compress(build_log.command_timings)
           stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
           stmt.bytes(5) = Properties.compress(build_log.task_statistics)
-          stmt.string(6) = cat_lines(build.sources)
-          stmt.string(7) = cat_lines(build.input_heaps)
-          stmt.string(8) = build.output_heap getOrElse ""
-          stmt.int(9) = build.return_code
+          stmt.bytes(6) = compress_errors(build_log.errors)
+          stmt.string(7) = cat_lines(build.sources)
+          stmt.string(8) = cat_lines(build.input_heaps)
+          stmt.string(9) = build.output_heap getOrElse ""
+          stmt.int(10) = build.return_code
           stmt.execute()
         })
       }
@@ -861,7 +871,8 @@
         session_timing = read_session_timing(db, name),
         command_timings = if (command_timings) read_command_timings(db, name) else Nil,
         ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
-        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil)
+        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
+        errors = uncompress_errors(read_bytes(db, name, Session_Info.errors)))
     }
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =

--- a/src/Pure/Tools/build.ML	Fri May 26 11:51:45 2017 +0200
+++ b/src/Pure/Tools/build.ML	Fri May 26 15:19:21 2017 +0200
@@ -220,10 +220,12 @@
     val _ = SHA1.test_samples ();
     val _ = Options.load_default ();
     val _ = Isabelle_Process.init_options ();
-    val args = decode_args (File.read (Path.explode args_file));
+    val args as Args {name, ...} = decode_args (File.read (Path.explode args_file));
+    fun error_message msg = writeln ("\ferror_message = " ^ encode_lines msg);
     val _ =
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
-        build_session args;
+        build_session args
+      handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn);
     val _ = Options.reset_default ();
   in () end;
 

--- a/src/Pure/library.ML	Fri May 26 11:51:45 2017 +0200
+++ b/src/Pure/library.ML	Fri May 26 15:19:21 2017 +0200
@@ -147,6 +147,8 @@
   val trim_split_lines: string -> string list
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
+  val encode_lines: string -> string
+  val decode_lines: string -> string
   val align_right: string -> int -> string -> string
   val match_string: string -> string -> bool
 
@@ -729,6 +731,9 @@
 
 fun translate_string f = String.translate (f o String.str);
 
+val encode_lines = translate_string (fn "\n" => "\v" | c => c);
+val decode_lines = translate_string (fn "\v" => "\n" | c => c);
+
 fun align_right c k s =
   let
     val _ = if size c <> 1 orelse size s > k