--- a/src/Pure/General/url.scala Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/General/url.scala Fri Apr 01 17:06:10 2022 +0200
@@ -14,8 +14,7 @@
import java.util.zip.GZIPInputStream
-object Url
-{
+object Url {
/* special characters */
def escape_special(c: Char): String =
@@ -32,8 +31,7 @@
/* make and check URLs */
- def apply(name: String): URL =
- {
+ def apply(name: String): URL = {
try { new URL(name) }
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
}
@@ -52,8 +50,7 @@
def file_name(url: URL): String =
Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString
- def trim_index(url: URL): URL =
- {
+ def trim_index(url: URL): URL = {
Library.try_unprefix("/index.html", url.toString) match {
case Some(u) => Url(u)
case None =>