# HG changeset patch
# User wenzelm
# Date 1661075114 -7200
# Node ID 17d51bdabdeddafc1fe069b94037d814e6314b96
# Parent  02b18f59f903a80c9c69216a4b1ebb9c61f46824
proper fonts_prefix (amending c14409948063): default is "" due to self-cancellation of dir;

diff -r 02b18f59f903 -r 17d51bdabded src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/Pure/Thy/html.scala	Sun Aug 21 11:45:14 2022 +0200
@@ -96,7 +96,7 @@
 
   /* href */
 
-  def relative_href(loc: Path, base: Option[Path] = None, reverse: Boolean = false): String = {
+  def relative_href(loc: Path, base: Option[Path] = None): String = {
     base match {
       case None =>
         val path = loc.expand
@@ -106,8 +106,7 @@
         val path1 = dir.absolute_file.toPath
         val path2 = loc.absolute_file.toPath
         try {
-          val java_path = if (reverse) path2.relativize(path1) else path1.relativize(path2)
-          val path = File.path(java_path.toFile)
+          val path = File.path(path1.relativize(path2).toFile)
           if (path.is_current) "" else path.implode
         }
         catch {
@@ -449,7 +448,8 @@
     structural: Boolean = true
   ): Unit = {
     Isabelle_System.make_directory(dir)
-    val fonts = fonts_css_dir(relative_href(dir, base = base, reverse = true))
+    val fonts_prefix = relative_href(base getOrElse dir, base = Some(dir))
+    val fonts = fonts_css_dir(fonts_prefix)
     File.write(dir + isabelle_css.base, fonts + "\n\n" + File.read(isabelle_css))
     File.write(dir + Path.basic(name),
       output_document(head, body, css = css, hidden = hidden, structural = structural))