# HG changeset patch # User wenzelm # Date 1700860961 -3600 # Node ID 156bfa6a28369f0284c42da2fc142376c09fc43d # Parent 1a9f3806987ddfb513a41b912e04c24adcf8aedb# Parent 1f34f6394383d2ab19732811c2fd762bae0c444c merged diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/General/file.scala --- 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) */ diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/General/json_api.scala --- 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) diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/General/mailman.scala --- 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 diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/General/socket_io.ML --- 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>\raise Fail "Cannot create Unix-domain socket on Windows"\ + \<^if_unix>\ + 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\ + +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; diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/General/url.scala --- 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 } diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/ROOT.ML --- 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"; diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/System/isabelle_process.scala diff -r 1a9f3806987d -r 156bfa6a2836 src/Pure/System/system_channel.scala --- 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() } diff -r 1a9f3806987d -r 156bfa6a2836 src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java --- 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); } diff -r 1a9f3806987d -r 156bfa6a2836 src/Tools/jEdit/src/session_build.scala --- 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)