src/Pure/Thy/sessions.scala
changeset 68086 9e1c670301b8
parent 68018 3747fe57eb67
child 68169 395432e7516e
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 04 22:26:25 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 05 13:56:51 2018 +0200
     1.3 @@ -1003,6 +1003,10 @@
     1.4  
     1.5      def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
     1.6  
     1.7 +    def output_database(name: String): Path = output_dir + database(name)
     1.8 +    def output_log(name: String): Path = output_dir + log(name)
     1.9 +    def output_log_gz(name: String): Path = output_dir + log_gz(name)
    1.10 +
    1.11  
    1.12      /* input */
    1.13  
    1.14 @@ -1028,6 +1032,15 @@
    1.15  
    1.16      /* session info */
    1.17  
    1.18 +    def init_session_info(db: SQL.Database, name: String)
    1.19 +    {
    1.20 +      db.transaction {
    1.21 +        db.create_table(Session_Info.table)
    1.22 +        db.using_statement(
    1.23 +          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.24 +      }
    1.25 +    }
    1.26 +
    1.27      def write_session_info(
    1.28        db: SQL.Database,
    1.29        name: String,
    1.30 @@ -1035,9 +1048,6 @@
    1.31        build: Build.Session_Info)
    1.32      {
    1.33        db.transaction {
    1.34 -        db.create_table(Session_Info.table)
    1.35 -        db.using_statement(
    1.36 -          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.37          db.using_statement(Session_Info.table.insert())(stmt =>
    1.38          {
    1.39            stmt.string(1) = name