# HG changeset patch
# User wenzelm
# Date 1658905386 -7200
# Node ID 84990c95712d1626012de5e538f89d6ebd1a9149
# Parent  953953504590a18c5aa143dba54ac365a5fc201a
clarified signature;

diff -r 953953504590 -r 84990c95712d src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Pure/General/file.scala	Wed Jul 27 09:03:06 2022 +0200
@@ -13,7 +13,7 @@
 import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
   FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, MalformedURLException}
+import java.net.{URI, URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
@@ -62,6 +62,12 @@
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def pwd(): Path = path(Path.current.absolute_file)
 
+  def uri(file: JFile): URI = file.toURI
+  def uri(path: Path): URI = path.file.toURI
+
+  def url(file: JFile): URL = uri(file).toURL
+  def url(path: Path): URL = url(path.file)
+
 
   /* relative paths */
 
diff -r 953953504590 -r 84990c95712d src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Pure/General/path.scala	Wed Jul 27 09:03:06 2022 +0200
@@ -11,7 +11,6 @@
 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
 
@@ -314,9 +313,6 @@
   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 953953504590 -r 84990c95712d src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed Jul 27 09:03:06 2022 +0200
@@ -42,7 +42,7 @@
                 thy_file <- Position.Def_File.unapply(props)
                 def_line <- Position.Def_Line.unapply(props)
                 source <- resources.source_file(thy_file)
-                uri = Path.explode(source).absolute_file.toURI
+                uri = File.uri(Path.explode(source).absolute_file)
               } yield HTML.link(uri.toString + "#" + def_line, body)
           }
         val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
diff -r 953953504590 -r 84990c95712d src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Jul 27 09:03:06 2022 +0200
@@ -66,7 +66,7 @@
                   thy_file <- Position.Def_File.unapply(props)
                   def_line <- Position.Def_Line.unapply(props)
                   source <- server.resources.source_file(thy_file)
-                  uri = Path.explode(source).absolute_file.toURI
+                  uri = File.uri(Path.explode(source).absolute_file)
                 } yield HTML.link(uri.toString + "#" + def_line, body)
             }
           val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
diff -r 953953504590 -r 84990c95712d src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Jul 26 20:35:42 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Jul 27 09:03:06 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").uri.toASCIIString
+        val file = File.uri(Path.explode("$ISABELLE_IDEA_ICONS")).toASCIIString
         "jar:" + file + "!/" + name
       }
       else name