src/Pure/Thy/sessions.scala
changeset 77543 97b5547f2b17
parent 77542 2da5562114c5
child 77544 42c1e5d4ed14
--- a/src/Pure/Thy/sessions.scala	Mon Mar 06 15:48:04 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 06 15:56:28 2023 +0100
@@ -1565,8 +1565,7 @@
 
         db.create_table(Document_Build.Data.table)
         db.execute_statement(
-          Document_Build.Data.table.delete(
-            sql = Document_Build.Data.session_name.where_equal(name)))
+          Document_Build.Data.table.delete(sql = Document_Build.Data.session_name.where_equal(name)))
       }
     }
 
@@ -1657,7 +1656,7 @@
 
     /* session sources */
 
-    def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit = {
+    def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit =
       for (source_file <- sources) {
         db.execute_statement(Sources.table.insert(), body =
           { stmt =>
@@ -1668,7 +1667,6 @@
             stmt.bytes(5) = source_file.body
           })
       }
-    }
 
     def read_sources(
       db: SQL.Database,