# 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("!" + content + "\u0000") } - finally { writer.close } + using(Files.newBufferedWriter(path, UTF8.charset))( + _.write("!" + 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)) } }