src/Pure/Thy/sessions.scala
changeset 65748 1f4a80e80c88
parent 65740 83388f09e9ab
child 65833 95fd3b9888e6
equal deleted inserted replaced
65747:5a3052b2095f 65748:1f4a80e80c88
   822         db.create_table(Session_Info.table)
   822         db.create_table(Session_Info.table)
   823         db.using_statement(
   823         db.using_statement(
   824           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
   824           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
   825         db.using_statement(Session_Info.table.insert())(stmt =>
   825         db.using_statement(Session_Info.table.insert())(stmt =>
   826         {
   826         {
   827           stmt.set_string(1, name)
   827           stmt.string(1) = name
   828           stmt.set_bytes(2, encode_properties(build_log.session_timing))
   828           stmt.bytes(2) = encode_properties(build_log.session_timing)
   829           stmt.set_bytes(3, compress_properties(build_log.command_timings))
   829           stmt.bytes(3) = compress_properties(build_log.command_timings)
   830           stmt.set_bytes(4, compress_properties(build_log.ml_statistics))
   830           stmt.bytes(4) = compress_properties(build_log.ml_statistics)
   831           stmt.set_bytes(5, compress_properties(build_log.task_statistics))
   831           stmt.bytes(5) = compress_properties(build_log.task_statistics)
   832           stmt.set_string(6, cat_lines(build.sources))
   832           stmt.string(6) = cat_lines(build.sources)
   833           stmt.set_string(7, cat_lines(build.input_heaps))
   833           stmt.string(7) = cat_lines(build.input_heaps)
   834           stmt.set_string(8, build.output_heap getOrElse "")
   834           stmt.string(8) = build.output_heap getOrElse ""
   835           stmt.set_int(9, build.return_code)
   835           stmt.int(9) = build.return_code
   836           stmt.execute()
   836           stmt.execute()
   837         })
   837         })
   838       }
   838       }
   839     }
   839     }
   840 
   840