more robust;
authorwenzelm
Sat, 20 Aug 2022 18:02:19 +0200
changeset 75930 e09abfd8ee80
parent 75929 811092261546
child 75931 7df33b58e741
more robust;
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 20 17:59:13 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 20 18:02:19 2022 +0200
@@ -60,7 +60,11 @@
       if (File.is_thy(file)) theory_html(theory) else file_html(file)
 
     def relative_link(dir: Path, file: Path): String =
-      try { File.path(dir.java_path.relativize(file.java_path).toFile).implode }
+      try {
+        val path1 = dir.absolute_file.toPath
+        val path2 = file.absolute_file.toPath
+        File.path(path1.relativize(path2).toFile).implode
+      }
       catch {
         case _: IllegalArgumentException =>
           error("Cannot relativize " + file + " wrt. " + dir)