src/Pure/System/standard_system.scala
changeset 44569 5130dfe1b7be
parent 44545 7f933761764b
child 44622 a41f618c641d
equal deleted inserted replaced
44565:93dcfcf91484 44569:5130dfe1b7be
    93 
    93 
    94   def slurp(stream: InputStream): String =
    94   def slurp(stream: InputStream): String =
    95     slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    95     slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    96 
    96 
    97   def read_file(file: File): String = slurp(new FileInputStream(file))
    97   def read_file(file: File): String = slurp(new FileInputStream(file))
    98 
       
    99   def try_read(files: Seq[File]): String =
       
   100   {
       
   101     val buf = new StringBuilder
       
   102     for {
       
   103       file <- files if file.isFile
       
   104       c <- (Source.fromFile(file) ++ Iterator.single('\n'))
       
   105     } buf.append(c)
       
   106     buf.toString
       
   107   }
       
   108 
    98 
   109   def write_file(file: File, text: CharSequence)
    99   def write_file(file: File, text: CharSequence)
   110   {
   100   {
   111     val writer =
   101     val writer =
   112       new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
   102       new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))