# HG changeset patch
# User wenzelm
# Date 1678114084 -3600
# Node ID 2da5562114c5d0920d3d0009a4436dacd4735e29
# Parent  9d9b30741fc4f1d075ec226b6ff13d998e26710e
clarified signature: more uniform operations;

diff -r 9d9b30741fc4 -r 2da5562114c5 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 06 15:38:50 2023 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 06 15:48:04 2023 +0100
@@ -321,7 +321,8 @@
   trait Database extends AutoCloseable {
     db =>
 
-    def is_server: Boolean
+    def is_sqlite: Boolean = isInstanceOf[SQLite.Database]
+    def is_postgresql: Boolean = isInstanceOf[PostgreSQL.Database]
 
     def rebuild(): Unit = ()
 
@@ -439,7 +440,6 @@
 
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
     override def toString: String = name
-    override def is_server: Boolean = false
     override def rebuild(): Unit = execute_statement("VACUUM")
 
     override def now(): Date = Date.now()
@@ -515,7 +515,6 @@
     port_forwarding: Option[SSH.Port_Forwarding]
   ) extends SQL.Database {
     override def toString: String = name
-    override def is_server: Boolean = true
 
     override def now(): Date = {
       val now = SQL.Column.date("now")
diff -r 9d9b30741fc4 -r 2da5562114c5 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Mar 06 15:38:50 2023 +0100
+++ b/src/Pure/Thy/export.scala	Mon Mar 06 15:48:04 2023 +0100
@@ -236,7 +236,7 @@
 
     def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
-        val args = if (db.is_server) args0.copy(compress = false) else args0
+        val args = if (db.is_postgresql) args0.copy(compress = false) else args0
         consumer.send(Entry.make(session_name, args, body, cache) -> args.strict)
       }
     }
diff -r 9d9b30741fc4 -r 2da5562114c5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 06 15:38:50 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 06 15:48:04 2023 +0100
@@ -1554,7 +1554,7 @@
         db.create_table(Session_Info.table)
         db.execute_statement(
           Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))
-        if (db.isInstanceOf[PostgreSQL.Database]) db.execute_statement(Session_Info.augment_table)
+        if (db.is_postgresql) db.execute_statement(Session_Info.augment_table)
 
         db.create_table(Sources.table)
         db.execute_statement(Sources.table.delete(sql = Sources.where_equal(name)))