--- a/src/Pure/General/file.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/General/file.scala Fri Nov 24 22:22:41 2023 +0100
@@ -13,7 +13,7 @@
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
FileVisitOption, FileVisitResult}
import java.nio.file.attribute.{BasicFileAttributes, PosixFilePermission}
-import java.net.{URI, URL, MalformedURLException}
+import java.net.{URI, URL}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.EnumSet
@@ -35,12 +35,13 @@
def standard_url(name: String): String =
try {
- val url = new URL(name)
- if (url.getProtocol == "file" && Url.is_wellformed_file(name))
+ val url = new URI(name).toURL
+ if (url.getProtocol == "file" && Url.is_wellformed_file(name)) {
standard_path(Url.parse_file(name))
+ }
else name
}
- catch { case _: MalformedURLException => standard_path(name) }
+ catch { case exn: Throwable if Url.is_malformed(exn) => standard_path(name) }
/* platform path (Windows or Posix) */
--- a/src/Pure/General/json_api.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/General/json_api.scala Fri Nov 24 22:22:41 2023 +0100
@@ -19,7 +19,7 @@
override def toString: String = url.toString
def get(route: String): HTTP.Content =
- HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
+ HTTP.Client.get(Url.resolve(url, route))
def get_root(route: String = ""): Root =
Root(get(if_proper(route, "/" + route)).json)
--- a/src/Pure/General/mailman.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/General/mailman.scala Fri Nov 24 22:22:41 2023 +0100
@@ -356,7 +356,7 @@
def list_tag: String = proper_string(tag).getOrElse(list_name)
- def read_text(href: String): String = Url.read(new URL(main_url, href))
+ def read_text(href: String): String = Url.read(Url.resolve(main_url, href))
def hrefs_text: List[String] =
"""href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(main_html).map(_.group(1)).toList
@@ -371,7 +371,7 @@
def get(target_dir: Path, href: String, progress: Progress = new Progress): Option[Path] = {
val dir = target_dir + Path.basic(list_name)
val path = dir + Path.explode(href)
- val url = new URL(main_url, href)
+ val url = Url.resolve(main_url, href)
val connection = url.openConnection
try {
val length = connection.getContentLengthLong
--- a/src/Pure/General/socket_io.ML Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/General/socket_io.ML Fri Nov 24 22:22:41 2023 +0100
@@ -8,7 +8,6 @@
signature SOCKET_IO =
sig
- val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
val open_streams: string -> BinIO.instream * BinIO.outstream
val with_streams: (BinIO.instream * BinIO.outstream -> 'a) -> string -> 'a
val with_streams': (BinIO.instream * BinIO.outstream -> 'a) -> string -> string -> 'a
@@ -20,15 +19,14 @@
fun close_permissive socket =
Socket.close socket handle OS.SysErr _ => ();
-fun make_streams socket =
+val buffer_size = 65536;
+
+fun make_streams socket_name socket =
let
- val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
- val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
-
val rd =
BinPrimIO.RD {
- name = name,
- chunkSize = 4096,
+ name = socket_name,
+ chunkSize = buffer_size,
readVec = SOME (fn n => Socket.recvVec (socket, n)),
readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
readVecNB = NONE,
@@ -46,8 +44,8 @@
val wr =
BinPrimIO.WR {
- name = name,
- chunkSize = 4096,
+ name = socket_name,
+ chunkSize = buffer_size,
writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
writeVecNB = NONE,
@@ -72,32 +70,52 @@
in (in_stream, out_stream) end;
+fun socket_name_inet name =
+ (case space_explode ":" name of
+ [h, p] =>
+ (case (NetHostDB.getByName h, Int.fromString p) of
+ (SOME host, SOME port) => SOME (host, port)
+ | _ => NONE)
+ | _ => NONE);
-fun open_streams socket_name =
+fun open_streams_inet (host, port) =
let
- fun err () = error ("Bad socket name: " ^ quote socket_name);
- val (host, port) =
- (case space_explode ":" socket_name of
- [h, p] =>
- (case NetHostDB.getByName h of SOME host => host | NONE => err (),
- case Int.fromString p of SOME port => port | NONE => err ())
- | _ => err ());
val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
- in make_streams socket end
- handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ socket_name);
+
+ val (socket_host, socket_port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
+ val socket_name = NetHostDB.toString socket_host ^ ":" ^ string_of_int socket_port;
+ in make_streams socket_name socket end;
+
+fun open_streams_unix path =
+ \<^if_windows>\<open>raise Fail "Cannot create Unix-domain socket on Windows"\<close>
+ \<^if_unix>\<open>
+ let
+ val socket_name = File.platform_path path;
+ val socket: Socket.active UnixSock.stream_sock = UnixSock.Strm.socket ();
+ val _ = Socket.connect (socket, UnixSock.toAddr socket_name);
+ in make_streams socket_name socket end\<close>
+
+fun open_streams name =
+ (case socket_name_inet name of
+ SOME inet => open_streams_inet inet
+ | NONE =>
+ (case try Path.explode name of
+ SOME path => open_streams_unix path
+ | NONE => error ("Bad socket name: " ^ quote name)))
+ handle OS.SysErr (msg, _) => error (msg ^ ": failed to open socket " ^ name);
fun with_streams f =
- Thread_Attributes.uninterruptible (fn run => fn socket_name =>
+ Thread_Attributes.uninterruptible (fn run => fn name =>
let
- val streams = open_streams socket_name;
+ val streams = open_streams name;
val result = Exn.capture (run f) streams;
val _ = BinIO.closeIn (#1 streams);
val _ = BinIO.closeOut (#2 streams);
in Exn.release result end);
-fun with_streams' f socket_name password =
+fun with_streams' f name password =
with_streams (fn streams =>
- (Byte_Message.write_line (#2 streams) (Bytes.string password); f streams)) socket_name;
+ (Byte_Message.write_line (#2 streams) (Bytes.string password); f streams)) name;
end;
--- a/src/Pure/General/url.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/General/url.scala Fri Nov 24 22:22:41 2023 +0100
@@ -31,10 +31,19 @@
/* make and check URLs */
- def apply(name: String): URL = {
- try { new URL(name) }
- catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
- }
+ def is_malformed(exn: Throwable): Boolean =
+ exn.isInstanceOf[MalformedURLException] ||
+ exn.isInstanceOf[URISyntaxException] ||
+ exn.isInstanceOf[IllegalArgumentException]
+
+ def apply(name: String): URL =
+ try { new URI(name).toURL }
+ catch {
+ case exn: Throwable if is_malformed(exn) => error("Malformed URL " + quote(name))
+ }
+
+ def resolve(url: URL, route: String): URL =
+ if (route.isEmpty) url else url.toURI.resolve(route).toURL
def is_wellformed(name: String): Boolean =
try { Url(name); true }
--- a/src/Pure/ROOT.ML Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/ROOT.ML Fri Nov 24 22:22:41 2023 +0100
@@ -100,7 +100,6 @@
ML_file "PIDE/byte_message.ML";
ML_file "PIDE/protocol_message.ML";
ML_file "PIDE/document_id.ML";
-ML_file "General/socket_io.ML";
ML_file "General/graph.ML";
@@ -301,6 +300,7 @@
ML_file "Proof/extraction.ML";
(*Isabelle system*)
+ML_file "General/socket_io.ML";
ML_file "PIDE/protocol_command.ML";
ML_file "System/java.ML";
ML_file "System/scala.ML";
--- a/src/Pure/System/system_channel.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Pure/System/system_channel.scala Fri Nov 24 22:22:41 2023 +0100
@@ -8,18 +8,45 @@
import java.io.{InputStream, OutputStream}
-import java.net.{ServerSocket, InetAddress}
+import java.net.{InetAddress, InetSocketAddress, ProtocolFamily, ServerSocket, SocketAddress,
+ StandardProtocolFamily, UnixDomainSocketAddress, StandardSocketOptions}
+import java.nio.channels.{ServerSocketChannel, Channels}
object System_Channel {
- def apply(): System_Channel = new System_Channel
+ def apply(unix_domain: Boolean = false): System_Channel =
+ if (unix_domain) new Unix else new Inet
+
+ val buffer_size: Integer = Integer.valueOf(65536)
+
+ class Inet extends System_Channel(StandardProtocolFamily.INET) {
+ server.bind(new InetSocketAddress(Server.localhost, 0), 50)
+ server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size)
+
+ override def address: String =
+ Server.print_address(server.getLocalAddress.asInstanceOf[InetSocketAddress].getPort)
+ }
+
+ class Unix extends System_Channel(StandardProtocolFamily.UNIX) {
+ private val socket_file = Isabelle_System.tmp_file("socket", initialized = false)
+ private val socket_file_name = socket_file.getPath
+
+ server.bind(UnixDomainSocketAddress.of(socket_file_name))
+ server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size)
+
+ override def address: String = socket_file_name
+ override def shutdown(): Unit = {
+ super.shutdown()
+ socket_file.delete
+ }
+ }
}
-class System_Channel private {
- private val server = new ServerSocket(0, 50, Server.localhost)
+abstract class System_Channel private(protocol_family: ProtocolFamily) {
+ protected val server: ServerSocketChannel = ServerSocketChannel.open(protocol_family)
- val address: String = Server.print_address(server.getLocalPort)
- val password: String = UUID.random().toString
+ def address: String
+ lazy val password: String = UUID.random().toString
override def toString: String = address
@@ -28,14 +55,15 @@
def rendezvous(): (OutputStream, InputStream) = {
val socket = server.accept
try {
- val out_stream = socket.getOutputStream
- val in_stream = socket.getInputStream
+ val out_stream = Channels.newOutputStream(socket)
+ val in_stream = Channels.newInputStream(socket)
- if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
- else {
- out_stream.close()
- in_stream.close()
- error("Failed to connect system channel: bad password")
+ Byte_Message.read_line(in_stream) match {
+ case Some(bs) if bs.text == password => (out_stream, in_stream)
+ case _ =>
+ out_stream.close()
+ in_stream.close()
+ error("Failed to connect system channel: bad password")
}
}
finally { shutdown() }
--- a/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Fri Nov 24 22:22:41 2023 +0100
@@ -45,7 +45,7 @@
String line, text = "";
try {
- rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
+ rd = new BufferedReader(new InputStreamReader((new URI(fname)).toURL().openConnection().getInputStream()));
} catch (Exception exn) {
rd = new FileReader(path + fname);
}
--- a/src/Tools/jEdit/src/session_build.scala Fri Nov 24 21:49:52 2023 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Fri Nov 24 22:22:41 2023 +0100
@@ -40,12 +40,12 @@
/* text */
- private val text = new TextArea {
- editable = false
- columns = 60
- rows = 24
- }
+ private val text = new TextArea
+ text.editable = false
+ text.columns = 60
+ text.rows = 24
text.font = GUI.copy_font((new Label).font)
+ text.caret.color = text.background
private val scroll_text = new ScrollPane(text)