# HG changeset patch
# User wenzelm
# Date 1543845582 -3600
# Node ID ed0824ef337ecfcd4286b86bb57230e526c94cbc
# Parent  fe2c16d9367a8f027298ea7d2177d01046fd9bd2
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
more uses of "using";

diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/bytes.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -95,11 +95,8 @@
 
   /* write */
 
-  def write(file: JFile, bytes: Bytes)
-  {
-    val stream = new FileOutputStream(file)
-    try { bytes.write_stream(stream) } finally { stream.close }
-  }
+  def write(file: JFile, bytes: Bytes): Unit =
+    using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/file.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -229,8 +229,7 @@
   def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))
-    val writer = new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset))
-    try { writer.append(text) } finally { writer.close }
+    using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
   }
 
   def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/graphics_file.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -58,8 +58,8 @@
   {
     import com.lowagie.text.{Document, Rectangle}
 
-    val out = new BufferedOutputStream(new FileOutputStream(file))
-    try {
+    using(new BufferedOutputStream(new FileOutputStream(file)))(out =>
+    {
       val document = new Document()
       try {
         document.setPageSize(new Rectangle(width, height))
@@ -76,8 +76,7 @@
         cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
       }
       finally { document.close() }
-    }
-    finally { out.close }
+    })
   }
 
 
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/http.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -45,18 +45,13 @@
     def request_uri: URI = http_exchange.getRequestURI
 
     def read_request(): Bytes =
-    {
-      val stream = http_exchange.getRequestBody
-      try { Bytes.read_stream(stream) } finally { stream.close }
-    }
+      using(http_exchange.getRequestBody)(Bytes.read_stream(_))
 
     def write_response(code: Int, response: Response)
     {
       http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
       http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
-
-      val stream = http_exchange.getResponseBody
-      try { response.bytes.write_stream(stream) } finally { stream.close }
+      using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
     }
   }
 
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/scan.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -451,7 +451,7 @@
     }
   }
 
-  abstract class Byte_Reader extends Reader[Char] { def close: Unit }
+  abstract class Byte_Reader extends Reader[Char] with AutoCloseable
 
   private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader =
   {
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/sha1.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -39,18 +39,19 @@
 
   def digest(file: JFile): Digest =
   {
-    val stream = new FileInputStream(file)
     val digest = MessageDigest.getInstance("SHA")
 
-    val buf = new Array[Byte](65536)
-    var m = 0
-    try {
-      do {
-        m = stream.read(buf, 0, buf.length)
-        if (m != -1) digest.update(buf, 0, m)
-      } while (m != -1)
-    }
-    finally { stream.close }
+    using(new FileInputStream(file))(stream =>
+    {
+      val buf = new Array[Byte](65536)
+      var m = 0
+      try {
+        do {
+          m = stream.read(buf, 0, buf.length)
+          if (m != -1) digest.update(buf, 0, m)
+        } while (m != -1)
+      }
+    })
 
     make_result(digest)
   }
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/sql.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -6,6 +6,7 @@
 
 package isabelle
 
+
 import java.time.OffsetDateTime
 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
@@ -189,6 +190,7 @@
   /* statements */
 
   class Statement private[SQL](val db: Database, val rep: PreparedStatement)
+    extends AutoCloseable
   {
     stmt =>
 
@@ -306,7 +308,7 @@
 
   /* database */
 
-  trait Database
+  trait Database extends AutoCloseable
   {
     db =>
 
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/ssh.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -184,7 +184,7 @@
     val local_host: String,
     val local_port: Int,
     val remote_host: String,
-    val remote_port: Int)
+    val remote_port: Int) extends AutoCloseable
   {
     override def toString: String =
       local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
@@ -211,7 +211,7 @@
 
   private val exec_wait_delay = Time.seconds(0.3)
 
-  class Exec private[SSH](session: Session, channel: ChannelExec)
+  class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable
   {
     override def toString: String = "exec " + session.toString
 
@@ -292,7 +292,7 @@
   class Session private[SSH](
     val options: Options,
     val session: JSch_Session,
-    on_close: () => Unit) extends System
+    on_close: () => Unit) extends System with AutoCloseable
   {
     def update_options(new_options: Options): Session =
       new Session(new_options, session, on_close)
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -156,10 +156,7 @@
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = name.path
-    if (path.is_file) {
-      val reader = Scan.byte_reader(path.file)
-      try { f(reader) } finally { reader.close }
-    }
+    if (path.is_file) using(Scan.byte_reader(path.file))(f)
     else if (name.node == name.theory)
       error("Cannot load theory " + quote(name.theory))
     else error ("Cannot load theory file " + path)
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/ROOT.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -10,7 +10,7 @@
   val error = Exn.error _
   def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
 
-  def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f)
+  def using[A <: AutoCloseable, B](a: A)(f: A => B): B = Library.using(a)(f)
   val space_explode = Library.space_explode _
   val split_lines = Library.split_lines _
   val cat_lines = Library.cat_lines _
@@ -25,4 +25,3 @@
   type UUID = java.util.UUID
   def UUID(): UUID = java.util.UUID.randomUUID()
 }
-
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/System/cygwin.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -46,9 +46,8 @@
           case link :: content :: rest =>
             val path = (new JFile(isabelle_root, link)).toPath
 
-            val writer = Files.newBufferedWriter(path, UTF8.charset)
-            try { writer.write("!<symlink>" + content + "\u0000") }
-            finally { writer.close }
+            using(Files.newBufferedWriter(path, UTF8.charset))(
+              _.write("!<symlink>" + content + "\u0000"))
 
             Files.setAttribute(path, "dos:system", true)
 
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -974,8 +974,8 @@
   def read_heap_digest(heap: Path): Option[String] =
   {
     if (heap.is_file) {
-      val file = FileChannel.open(heap.file.toPath, StandardOpenOption.READ)
-      try {
+      using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
+      {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length
         if (len >= n) {
@@ -998,8 +998,7 @@
           else None
         }
         else None
-      }
-      finally { file.close }
+      })
     }
     else None
   }
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -161,7 +161,7 @@
       new Connection(socket)
   }
 
-  class Connection private(socket: Socket)
+  class Connection private(socket: Socket) extends AutoCloseable
   {
     override def toString: String = socket.toString
 
@@ -220,6 +220,7 @@
   /* context with output channels */
 
   class Context private[Server](val server: Server, connection: Connection)
+    extends AutoCloseable
   {
     context =>
 
diff -r fe2c16d9367a -r ed0824ef337e src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/library.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -16,12 +16,10 @@
 {
   /* resource management */
 
-  def using[A <: { def close() }, B](x: A)(f: A => B): B =
+  def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
   {
-    import scala.language.reflectiveCalls
-
-    try { f(x) }
-    finally { if (x != null) x.close() }
+    try { f(a) }
+    finally { if (a != null) a.close() }
   }
 
 
diff -r fe2c16d9367a -r ed0824ef337e src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -140,11 +140,8 @@
     val file = node_file(name)
     get_model(file) match {
       case Some(model) => f(Scan.char_reader(model.content.text))
-      case None if file.isFile =>
-        val reader = Scan.byte_reader(file)
-        try { f(reader) } finally { reader.close }
-      case None =>
-        error("No such file: " + quote(file.toString))
+      case None if file.isFile => using(Scan.byte_reader(file))(f)
+      case None => error("No such file: " + quote(file.toString))
     }
   }