tuned signature;
authorwenzelm
Sun May 06 23:01:45 2018 +0200 (15 months ago)
changeset 680910c7820590236
parent 68090 7c8ed28dd40a
child 68092 888d35a19866
tuned signature;
src/Pure/General/sql.scala
src/Pure/System/process_result.scala
     1.1 --- a/src/Pure/General/sql.scala	Sun May 06 22:15:52 2018 +0200
     1.2 +++ b/src/Pure/General/sql.scala	Sun May 06 23:01:45 2018 +0200
     1.3 @@ -120,7 +120,8 @@
     1.4      def defined: String = ident + " IS NOT NULL"
     1.5      def undefined: String = ident + " IS NULL"
     1.6  
     1.7 -    def where_equal(s: String): Source = "WHERE " + ident + " = " + string(s)
     1.8 +    def equal(s: String): Source = ident + " = " + string(s)
     1.9 +    def where_equal(s: String): Source = "WHERE " + equal(s)
    1.10  
    1.11      override def toString: Source = ident
    1.12    }
     2.1 --- a/src/Pure/System/process_result.scala	Sun May 06 22:15:52 2018 +0200
     2.2 +++ b/src/Pure/System/process_result.scala	Sun May 06 23:01:45 2018 +0200
     2.3 @@ -15,7 +15,8 @@
     2.4  {
     2.5    def out: String = cat_lines(out_lines)
     2.6    def err: String = cat_lines(err_lines)
     2.7 -  def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
     2.8 +  def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs)
     2.9 +  def error(err: String): Process_Result = errors(List(err))
    2.10  
    2.11    def was_timeout: Process_Result = copy(rc = 1, timeout = true)
    2.12