# HG changeset patch
# User wenzelm
# Date 1658752845 -7200
# Node ID c79df6dc2803d0a70652ff691ab4ae929445469b
# Parent  14e22b525b137062f9be59c0fd53ffa1f54a4450
clarified signature;

diff -r 14e22b525b13 -r c79df6dc2803 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Jul 25 11:19:08 2022 +0200
+++ b/src/Pure/General/path.scala	Mon Jul 25 14:40:45 2022 +0200
@@ -11,6 +11,7 @@
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
 import java.nio.file.{Path => JPath}
+import java.net.{URI, URL}
 
 import scala.util.matching.Regex
 
@@ -313,6 +314,9 @@
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
+  def uri: URI = file.toURI
+  def url: URL = uri.toURL
+
   def java_path: JPath = file.toPath
 
   def absolute_file: JFile = File.absolute(file)
diff -r 14e22b525b13 -r c79df6dc2803 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Jul 25 11:19:08 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Jul 25 14:40:45 2022 +0200
@@ -287,7 +287,7 @@
   def load_icon(name: String): Icon = {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString
+        val file = Path.explode("$ISABELLE_IDEA_ICONS").uri.toASCIIString
         "jar:" + file + "!/" + name
       }
       else name