# HG changeset patch
# User wenzelm
# Date 1661022841 -7200
# Node ID c14409948063291f493bf6dadde8c777d543f840
# Parent  dfd007aeb66ff942eb571b2fc05ffdb5507ab9f0
clarified signature: just one common operation;

diff -r dfd007aeb66f -r c14409948063 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Aug 20 18:55:48 2022 +0200
+++ b/src/Pure/Thy/html.scala	Sat Aug 20 21:14:01 2022 +0200
@@ -94,6 +94,30 @@
   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
 
 
+  /* href */
+
+  def relative_href(loc: Path, base: Option[Path] = None, reverse: Boolean = false): String = {
+    base match {
+      case None =>
+        val path = loc.expand
+        if (path.is_absolute) Exn.error("Relative href expected: " + path)
+        else if (path.is_current) "" else path.implode
+      case Some(dir) =>
+        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)
+          if (path.is_current) "" else path.implode
+        }
+        catch {
+          case _: IllegalArgumentException =>
+            Exn.error("Failed to relativize href " + path2 + " with wrt. base " + path1)
+        }
+    }
+  }
+
+
   /* output text with control symbols */
 
   private val control: Map[Symbol.Symbol, Operator] =
@@ -416,14 +440,6 @@
 
   /* document directory context (fonts + css) */
 
-  def relative_prefix(dir: Path, base: Option[Path]): String =
-    base match {
-      case None => ""
-      case Some(base_dir) =>
-        val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile)
-        if (path.is_current) "" else path.implode + "/"
-    }
-
   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
@@ -433,8 +449,8 @@
     structural: Boolean = true
   ): Unit = {
     Isabelle_System.make_directory(dir)
-    val prefix = relative_prefix(dir, base)
-    File.write(dir + isabelle_css.base, fonts_css_dir(prefix) + "\n\n" + File.read(isabelle_css))
+    val fonts = fonts_css_dir(relative_href(dir, base = base, reverse = true))
+    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))
   }
diff -r dfd007aeb66f -r c14409948063 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 20 18:55:48 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 20 21:14:01 2022 +0200
@@ -59,17 +59,6 @@
     def smart_html(theory: Document_Info.Theory, file: String): Path =
       if (File.is_thy(file)) theory_html(theory) else file_html(file)
 
-    def relative_link(dir: Path, file: Path): String =
-      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)
-      }
-
 
     /* HTML content */
 
@@ -184,7 +173,7 @@
               for (theory <- html_context.theory_by_name(session_name, thy_name))
               yield {
                 val html_path = session_dir + html_context.theory_html(theory)
-                val html_link = html_context.relative_link(node_dir, html_path)
+                val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.link(html_link, body)
               }
             case Entity_Ref(def_file, kind, name) =>
@@ -205,7 +194,7 @@
               }
               yield {
                 val html_path = session_dir + html_context.smart_html(theory, def_file)
-                val html_link = html_context.relative_link(node_dir, html_path)
+                val html_link = HTML.relative_href(html_path, base = Some(node_dir))
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }
             case _ => None
@@ -519,7 +508,7 @@
 
           val file_html = session_dir + html_context.file_html(file_name)
           val file_dir = file_html.dir
-          val html_link = html_context.relative_link(session_dir, file_html)
+          val html_link = HTML.relative_href(file_html, base = Some(session_dir))
           val html =
             html_context.source(
               node_context(file_name, file_dir).make_html(thy_elements, xml))