tuned signature: more operations;
authorwenzelm
Wed, 14 Jun 2023 11:18:25 +0200
changeset 78152 d4f387339494
parent 78151 2fdf3d8a94e6
child 78153 55a6aa77f3d8
tuned signature: more operations;
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Jun 08 14:45:31 2023 +0200
+++ b/src/Pure/General/sql.scala	Wed Jun 14 11:18:25 2023 +0200
@@ -72,7 +72,9 @@
   val TRUE: Source = "TRUE"
   val FALSE: Source = "FALSE"
 
-  def equal(sql: Source, s: String): Source = sql + " = " + string(s)
+  def equal(sql: Source, x: Int): Source = sql + " = " + x
+  def equal(sql: Source, x: Long): Source = sql + " = " + x
+  def equal(sql: Source, x: String): Source = sql + " = " + string(x)
 
   def member(sql: Source, set: Iterable[String]): Source =
     if (set.isEmpty) FALSE
@@ -146,10 +148,15 @@
     def defined: String = ident + " IS NOT NULL"
     def undefined: String = ident + " IS NULL"
 
-    def equal(s: String): Source = SQL.equal(ident, s)
+    def equal(x: Int): Source = SQL.equal(ident, x)
+    def equal(x: Long): Source = SQL.equal(ident, x)
+    def equal(x: String): Source = SQL.equal(ident, x)
+
+    def where_equal(x: Int): Source = SQL.where(equal(x))
+    def where_equal(x: Long): Source = SQL.where(equal(x))
+    def where_equal(x: String): Source = SQL.where(equal(x))
+
     def member(set: Iterable[String]): Source = SQL.member(ident, set)
-
-    def where_equal(s: String): Source = SQL.where(equal(s))
     def where_member(set: Iterable[String]): Source = SQL.where(member(set))
 
     def max: Column = copy(expr = "MAX(" + ident + ")")