src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Mon Mar 09 16:58:23 2020 +0100
+++ b/src/Pure/General/file.scala	Mon Mar 09 19:35:07 2020 +0100
@@ -231,6 +231,9 @@
 
   /* write */
 
+  def writer(file: JFile): BufferedWriter =
+    new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
+
   def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))