# HG changeset patch
# User wenzelm
# Date 1686734305 -7200
# Node ID d4f387339494d7bd523055400f66c4492ebcca9a
# Parent  2fdf3d8a94e6bb27933a1f7426a87aac89b25ef6
tuned signature: more operations;

diff -r 2fdf3d8a94e6 -r d4f387339494 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 + ")")