src/Pure/Thy/html.scala
changeset 75940 c6edbc025fae
parent 75939 87f0adcb7e10
child 76618 aeded421d374
equal deleted inserted replaced
75939:87f0adcb7e10 75940:c6edbc025fae
    94   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
    94   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
    95 
    95 
    96 
    96 
    97   /* href */
    97   /* href */
    98 
    98 
    99   def relative_href(loc: Path, base: Option[Path] = None): String = {
    99   def relative_href(location: Path, base: Option[Path] = None): String = {
   100     val path =
   100     val path =
   101       base match {
   101       base match {
   102         case None =>
   102         case None =>
   103           val path = loc.expand
   103           val path = location.expand
   104           if (path.is_absolute) Exn.error("Relative href expected: " + path) else path
   104           if (path.is_absolute) Exn.error("Relative href location expected: " + path) else path
   105         case Some(dir) =>
   105         case Some(base_dir) =>
   106           val path1 = dir.absolute_file.toPath
   106           val path1 = base_dir.absolute_file.toPath
   107           val path2 = loc.absolute_file.toPath
   107           val path2 = location.absolute_file.toPath
   108           try { File.path(path1.relativize(path2).toFile) }
   108           try { File.path(path1.relativize(path2).toFile) }
   109           catch {
   109           catch {
   110             case _: IllegalArgumentException =>
   110             case _: IllegalArgumentException =>
   111               Exn.error("Failed to relativize href " + path2 + " with wrt. base " + path1)
   111               Exn.error("Failed to relativize href location " + path2 + " with wrt. base " + path1)
   112           }
   112           }
   113       }
   113       }
   114     if (path.is_current) "" else path.implode
   114     if (path.is_current) "" else path.implode
   115   }
   115   }
   116 
   116 
   437 
   437 
   438   /* document directory context (fonts + css) */
   438   /* document directory context (fonts + css) */
   439 
   439 
   440   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
   440   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
   441 
   441 
   442   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
   442   def write_document(base_dir: Path, name: String, head: XML.Body, body: XML.Body,
   443     base: Option[Path] = None,
   443     root: Option[Path] = None,
   444     css: String = isabelle_css.file_name,
   444     css: String = isabelle_css.file_name,
   445     hidden: Boolean = true,
   445     hidden: Boolean = true,
   446     structural: Boolean = true
   446     structural: Boolean = true
   447   ): Unit = {
   447   ): Unit = {
   448     Isabelle_System.make_directory(dir)
   448     Isabelle_System.make_directory(base_dir)
   449     val fonts_prefix = relative_href(base getOrElse dir, base = Some(dir))
   449     val fonts_prefix = relative_href(root getOrElse base_dir, base = Some(base_dir))
   450     val fonts = fonts_css_dir(fonts_prefix)
   450     val fonts = fonts_css_dir(fonts_prefix)
   451     File.write(dir + isabelle_css.base, fonts + "\n\n" + File.read(isabelle_css))
   451     File.write(base_dir + isabelle_css.base, fonts + "\n\n" + File.read(isabelle_css))
   452     File.write(dir + Path.basic(name),
   452     File.write(base_dir + Path.basic(name),
   453       output_document(head, body, css = css, hidden = hidden, structural = structural))
   453       output_document(head, body, css = css, hidden = hidden, structural = structural))
   454   }
   454   }
   455 }
   455 }