src/Pure/Thy/sessions.scala
changeset 66873 9953ae603a23
parent 66857 f8f42289c4df
child 66914 fb3f13a9c756
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -829,11 +829,13 @@
     1.4      // Build_Log.Session_Info
     1.5      val session_timing = SQL.Column.bytes("session_timing")
     1.6      val command_timings = SQL.Column.bytes("command_timings")
     1.7 +    val theory_timings = SQL.Column.bytes("theory_timings")
     1.8      val ml_statistics = SQL.Column.bytes("ml_statistics")
     1.9      val task_statistics = SQL.Column.bytes("task_statistics")
    1.10      val errors = SQL.Column.bytes("errors")
    1.11      val build_log_columns =
    1.12 -      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
    1.13 +      List(session_name, session_timing, command_timings, theory_timings,
    1.14 +        ml_statistics, task_statistics, errors)
    1.15  
    1.16      // Build.Session_Info
    1.17      val sources = SQL.Column.string("sources")
    1.18 @@ -926,13 +928,14 @@
    1.19            stmt.string(1) = name
    1.20            stmt.bytes(2) = Properties.encode(build_log.session_timing)
    1.21            stmt.bytes(3) = Properties.compress(build_log.command_timings)
    1.22 -          stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.23 -          stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.24 -          stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    1.25 -          stmt.string(7) = build.sources
    1.26 -          stmt.string(8) = cat_lines(build.input_heaps)
    1.27 -          stmt.string(9) = build.output_heap getOrElse ""
    1.28 -          stmt.int(10) = build.return_code
    1.29 +          stmt.bytes(4) = Properties.compress(build_log.theory_timings)
    1.30 +          stmt.bytes(5) = Properties.compress(build_log.ml_statistics)
    1.31 +          stmt.bytes(6) = Properties.compress(build_log.task_statistics)
    1.32 +          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors)
    1.33 +          stmt.string(8) = build.sources
    1.34 +          stmt.string(9) = cat_lines(build.input_heaps)
    1.35 +          stmt.string(10) = build.output_heap getOrElse ""
    1.36 +          stmt.int(11) = build.return_code
    1.37            stmt.execute()
    1.38          })
    1.39        }
    1.40 @@ -944,6 +947,9 @@
    1.41      def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
    1.42        read_properties(db, name, Session_Info.command_timings)
    1.43  
    1.44 +    def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
    1.45 +      read_properties(db, name, Session_Info.theory_timings)
    1.46 +
    1.47      def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
    1.48        read_properties(db, name, Session_Info.ml_statistics)
    1.49