clarified signature: terminology of "base" (here) vs. "root" (there);
authorwenzelm
Sun, 21 Aug 2022 11:52:51 +0200
changeset 75940 c6edbc025fae
parent 75939 87f0adcb7e10
child 75941 4bbbbaa656f1
clarified signature: terminology of "base" (here) vs. "root" (there);
src/Pure/Thy/html.scala
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/html.scala	Sun Aug 21 11:48:14 2022 +0200
+++ b/src/Pure/Thy/html.scala	Sun Aug 21 11:52:51 2022 +0200
@@ -96,19 +96,19 @@
 
   /* href */
 
-  def relative_href(loc: Path, base: Option[Path] = None): String = {
+  def relative_href(location: Path, base: Option[Path] = None): String = {
     val path =
       base match {
         case None =>
-          val path = loc.expand
-          if (path.is_absolute) Exn.error("Relative href expected: " + path) else path
-        case Some(dir) =>
-          val path1 = dir.absolute_file.toPath
-          val path2 = loc.absolute_file.toPath
+          val path = location.expand
+          if (path.is_absolute) Exn.error("Relative href location expected: " + path) else path
+        case Some(base_dir) =>
+          val path1 = base_dir.absolute_file.toPath
+          val path2 = location.absolute_file.toPath
           try { File.path(path1.relativize(path2).toFile) }
           catch {
             case _: IllegalArgumentException =>
-              Exn.error("Failed to relativize href " + path2 + " with wrt. base " + path1)
+              Exn.error("Failed to relativize href location " + path2 + " with wrt. base " + path1)
           }
       }
     if (path.is_current) "" else path.implode
@@ -439,17 +439,17 @@
 
   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
 
-  def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
-    base: Option[Path] = None,
+  def write_document(base_dir: Path, name: String, head: XML.Body, body: XML.Body,
+    root: Option[Path] = None,
     css: String = isabelle_css.file_name,
     hidden: Boolean = true,
     structural: Boolean = true
   ): Unit = {
-    Isabelle_System.make_directory(dir)
-    val fonts_prefix = relative_href(base getOrElse dir, base = Some(dir))
+    Isabelle_System.make_directory(base_dir)
+    val fonts_prefix = relative_href(root getOrElse base_dir, base = Some(base_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),
+    File.write(base_dir + isabelle_css.base, fonts + "\n\n" + File.read(isabelle_css))
+    File.write(base_dir + Path.basic(name),
       output_document(head, body, css = css, hidden = hidden, structural = structural))
   }
 }
--- a/src/Pure/Thy/presentation.scala	Sun Aug 21 11:48:14 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sun Aug 21 11:52:51 2022 +0200
@@ -384,7 +384,7 @@
                 (List(HTML.link(name + "/index.html", HTML.text(name))),
                   if (descr == "") Nil
                   else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))),
-      base = Some(presentation_dir))
+      root = Some(presentation_dir))
   }
 
   def update_root(presentation_dir: Path): Unit = {
@@ -516,14 +516,14 @@
           val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short)
           HTML.write_document(file_dir, file_html.file_name,
             List(HTML.title(file_title)), List(html_context.head(file_title), html),
-            base = Some(html_context.root_dir))
+            root = Some(html_context.root_dir))
           List(HTML.link(html_link, HTML.text(file_title)))
         }
 
       val thy_title = "Theory " + theory.print_short
       HTML.write_document(session_dir, html_context.theory_html(theory).implode,
         List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html),
-        base = Some(html_context.root_dir))
+        root = Some(html_context.root_dir))
 
       List(HTML.link(html_context.theory_html(theory),
         HTML.text(theory.print_short) :::
@@ -537,6 +537,6 @@
         List(HTML.title(title + Isabelle_System.isabelle_heading())),
         html_context.head(title, List(HTML.par(document_links))) ::
           html_context.contents("Theories", theories),
-        base = Some(html_context.root_dir))
+        root = Some(html_context.root_dir))
   }
 }