src/Pure/General/bytes.scala
changeset 68108 2277fe496d78
parent 68106 a514e29db980
child 68149 9a4a6adb95b5
equal deleted inserted replaced
68107:3687109009c4 68108:2277fe496d78
    54       catch { case _: NumberFormatException => err() }
    54       catch { case _: NumberFormatException => err() }
    55     }
    55     }
    56     new Bytes(a, 0, n)
    56     new Bytes(a, 0, n)
    57   }
    57   }
    58 
    58 
       
    59   def base64(s: String): Bytes =
       
    60   {
       
    61     val a = Base64.getDecoder.decode(s)
       
    62     new Bytes(a, 0, a.length)
       
    63   }
       
    64 
    59 
    65 
    60   /* read */
    66   /* read */
    61 
    67 
    62   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
    68   def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
    63     if (limit == 0) empty
    69     if (limit == 0) empty