diff -r b25ccd85b1fd -r 9e1c670301b8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri May 04 22:26:25 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Sat May 05 13:56:51 2018 +0200 @@ -1003,6 +1003,10 @@ def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } + def output_database(name: String): Path = output_dir + database(name) + def output_log(name: String): Path = output_dir + log(name) + def output_log_gz(name: String): Path = output_dir + log_gz(name) + /* input */ @@ -1028,6 +1032,15 @@ /* session info */ + def init_session_info(db: SQL.Database, name: String) + { + db.transaction { + db.create_table(Session_Info.table) + db.using_statement( + Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) + } + } + def write_session_info( db: SQL.Database, name: String, @@ -1035,9 +1048,6 @@ build: Build.Session_Info) { db.transaction { - db.create_table(Session_Info.table) - db.using_statement( - Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) db.using_statement(Session_Info.table.insert())(stmt => { stmt.string(1) = name