src/Pure/Thy/sessions.scala
changeset 65937 fde7b5d209d5
parent 65934 5f202ba9f590
child 65938 1b297ce1e8aa
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 26 19:39:02 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 26 20:52:01 2017 +0200
     1.3 @@ -815,14 +815,6 @@
     1.4  
     1.5      /* session info */
     1.6  
     1.7 -    def compress_errors(errors: List[String]): Option[Bytes] =
     1.8 -      if (errors.isEmpty) None
     1.9 -      else Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).compress())
    1.10 -
    1.11 -    def uncompress_errors(bytes: Bytes): List[String] =
    1.12 -      if (bytes.isEmpty) Nil
    1.13 -      else XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress().text))
    1.14 -
    1.15      def write_session_info(
    1.16        db: SQL.Database,
    1.17        name: String,
    1.18 @@ -840,7 +832,7 @@
    1.19            stmt.bytes(3) = Properties.compress(build_log.command_timings)
    1.20            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.21            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.22 -          stmt.bytes(6) = compress_errors(build_log.errors)
    1.23 +          stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    1.24            stmt.string(7) = cat_lines(build.sources)
    1.25            stmt.string(8) = cat_lines(build.input_heaps)
    1.26            stmt.string(9) = build.output_heap getOrElse ""
    1.27 @@ -862,6 +854,9 @@
    1.28      def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
    1.29        read_properties(db, name, Session_Info.task_statistics)
    1.30  
    1.31 +    def read_errors(db: SQL.Database, name: String): List[String] =
    1.32 +      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
    1.33 +
    1.34      def read_build_log(db: SQL.Database, name: String,
    1.35        command_timings: Boolean = false,
    1.36        ml_statistics: Boolean = false,
    1.37 @@ -872,7 +867,7 @@
    1.38          command_timings = if (command_timings) read_command_timings(db, name) else Nil,
    1.39          ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
    1.40          task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
    1.41 -        errors = uncompress_errors(read_bytes(db, name, Session_Info.errors)))
    1.42 +        errors = read_errors(db, name).map(Library.decode_lines(_)))
    1.43      }
    1.44  
    1.45      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =