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 } |