src/Pure/Thy/sessions.scala
changeset 65934 5f202ba9f590
parent 65857 5d29d93766ef
child 65937 fde7b5d209d5
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 26 11:51:45 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 26 15:19:21 2017 +0200
     1.3 @@ -735,8 +735,9 @@
     1.4      val command_timings = SQL.Column.bytes("command_timings")
     1.5      val ml_statistics = SQL.Column.bytes("ml_statistics")
     1.6      val task_statistics = SQL.Column.bytes("task_statistics")
     1.7 +    val errors = SQL.Column.bytes("errors")
     1.8      val build_log_columns =
     1.9 -      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.10 +      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
    1.11  
    1.12      // Build.Session_Info
    1.13      val sources = SQL.Column.string("sources")
    1.14 @@ -814,6 +815,14 @@
    1.15  
    1.16      /* session info */
    1.17  
    1.18 +    def compress_errors(errors: List[String]): Option[Bytes] =
    1.19 +      if (errors.isEmpty) None
    1.20 +      else Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).compress())
    1.21 +
    1.22 +    def uncompress_errors(bytes: Bytes): List[String] =
    1.23 +      if (bytes.isEmpty) Nil
    1.24 +      else XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress().text))
    1.25 +
    1.26      def write_session_info(
    1.27        db: SQL.Database,
    1.28        name: String,
    1.29 @@ -831,10 +840,11 @@
    1.30            stmt.bytes(3) = Properties.compress(build_log.command_timings)
    1.31            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.32            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.33 -          stmt.string(6) = cat_lines(build.sources)
    1.34 -          stmt.string(7) = cat_lines(build.input_heaps)
    1.35 -          stmt.string(8) = build.output_heap getOrElse ""
    1.36 -          stmt.int(9) = build.return_code
    1.37 +          stmt.bytes(6) = compress_errors(build_log.errors)
    1.38 +          stmt.string(7) = cat_lines(build.sources)
    1.39 +          stmt.string(8) = cat_lines(build.input_heaps)
    1.40 +          stmt.string(9) = build.output_heap getOrElse ""
    1.41 +          stmt.int(10) = build.return_code
    1.42            stmt.execute()
    1.43          })
    1.44        }
    1.45 @@ -861,7 +871,8 @@
    1.46          session_timing = read_session_timing(db, name),
    1.47          command_timings = if (command_timings) read_command_timings(db, name) else Nil,
    1.48          ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
    1.49 -        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil)
    1.50 +        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
    1.51 +        errors = uncompress_errors(read_bytes(db, name, Session_Info.errors)))
    1.52      }
    1.53  
    1.54      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =