clarified signature: prefer enum types;

--- a/src/Pure/General/sql.scala	Tue Aug 29 16:18:29 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Aug 29 16:30:07 2023 +0200
@@ -95,26 +95,24 @@
 
   /* types */
 
-  object Type extends Enumeration {
-    val Boolean = Value("BOOLEAN")
-    val Int = Value("INTEGER")
-    val Long = Value("BIGINT")
-    val Double = Value("DOUBLE PRECISION")
-    val String = Value("TEXT")
-    val Bytes = Value("BLOB")
-    val Date = Value("TIMESTAMP WITH TIME ZONE")
+  enum Type { case Boolean, Int, Long, Double, String, Bytes, Date }
+
+  val sql_type_postgresql: Type => Source = {
+    case Type.Boolean => "BOOLEAN"
+    case Type.Int => "INTEGER"
+    case Type.Long => "BIGINT"
+    case Type.Double => "DOUBLE PRECISION"
+    case Type.String => "TEXT"
+    case Type.Bytes => "BYTEA"
+    case Type.Date => "TIMESTAMP WITH TIME ZONE"
   }
 
-  def sql_type_default(T: Type.Value): Source = T.toString
-
-  def sql_type_sqlite(T: Type.Value): Source =
-    if (T == Type.Boolean) "INTEGER"
-    else if (T == Type.Date) "TEXT"
-    else sql_type_default(T)
-
-  def sql_type_postgresql(T: Type.Value): Source =
-    if (T == Type.Bytes) "BYTEA"
-    else sql_type_default(T)
+  val sql_type_sqlite: Type => Source = {
+    case Type.Boolean => "INTEGER"
+    case Type.Bytes => "BLOB"
+    case Type.Date => "TEXT"
+    case t => sql_type_postgresql(t)
+  }
 
 
   /* columns */
@@ -138,7 +136,7 @@
 
   sealed case class Column(
     name: String,
-    T: Type.Value,
+    T: Type,
     strict: Boolean = false,
     primary_key: Boolean = false,
     expr: SQL.Source = ""
@@ -152,7 +150,7 @@
       if (expr == "") SQL.ident(name)
       else enclose(expr) + " AS " + SQL.ident(name)
 
-    def decl(sql_type: Type.Value => Source): Source =
+    def decl(sql_type: Type => Source): Source =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
     def defined: String = ident + " IS NOT NULL"
@@ -194,7 +192,7 @@
 
     def query_named: Source = query + " AS " + SQL.ident(name)
 
-    def create(sql_type: Type.Value => Source): Source = {
+    def create(sql_type: Type => Source): Source = {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
           case Nil => Nil
@@ -407,7 +405,7 @@
 
     /* types */
 
-    def sql_type(T: Type.Value): Source
+    def sql_type(T: Type): Source
 
 
     /* connection */
@@ -627,7 +625,7 @@
 
     override def now(): Date = Date.now()
 
-    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
+    def sql_type(T: SQL.Type): SQL.Source = SQL.sql_type_sqlite(T)
 
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
       if (date == null) stmt.string(i) = (null: String)
@@ -751,7 +749,7 @@
         .getOrElse(error("Failed to get current date/time from database server " + toString))
     }
 
-    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
+    def sql_type(T: SQL.Type): SQL.Source = SQL.sql_type_postgresql(T)
 
     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
     def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =