static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
more uses of "using";
--- 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)
}
--- 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)
--- 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 }
+ })
}
--- 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(_))
}
}
--- 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 =
{
--- 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)
}
--- 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 =>
--- 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)
--- 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)
--- 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()
}
-
--- 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)
--- 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
}
--- 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 =>
--- 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() }
}
--- 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))
}
}