# HG changeset patch
# User wenzelm
# Date 1700820631 -3600
# Node ID 24d04dd5bf017fb04e9be95b0e464bb38779cc42
# Parent  8cc1ae43e12e37a48fd3d43c0229930f1655dab1
more robust exception handling (amending 8cc1ae43e12e);

diff -r 8cc1ae43e12e -r 24d04dd5bf01 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Nov 23 11:40:49 2023 +0100
+++ b/src/Pure/General/file.scala	Fri Nov 24 11:10:31 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, URISyntaxException}
+import java.net.{URI, URL}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
@@ -41,9 +41,7 @@
       }
       else name
     }
-    catch {
-      case _: MalformedURLException | _: URISyntaxException => standard_path(name)
-    }
+    catch { case exn: Throwable if Url.is_malformed(exn) => standard_path(name) }
 
 
   /* platform path (Windows or Posix) */
diff -r 8cc1ae43e12e -r 24d04dd5bf01 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Thu Nov 23 11:40:49 2023 +0100
+++ b/src/Pure/General/url.scala	Fri Nov 24 11:10:31 2023 +0100
@@ -31,11 +31,15 @@
 
   /* make and check URLs */
 
+  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 _: MalformedURLException | _: URISyntaxException =>
-        error("Malformed URL " + quote(name))
+      case exn: Throwable if is_malformed(exn) => error("Malformed URL " + quote(name))
     }
 
   def resolve(url: URL, route: String): URL =