src/Pure/General/url.scala
changeset 75393 87ebf5a50283
parent 73417 1dcc2b228b8b
child 76354 908433a347d1
--- 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 =>