# HG changeset patch # User wenzelm # Date 1636148609 -3600 # Node ID d73a7e3c618c5e919ae5dcd7982d6a2bf3c5d4df # Parent b2df121ccfc1187e226e24dde06ca484bba98dfb avoid multiple copies of fonts; proper fonts prefix for aux. files; diff -r b2df121ccfc1 -r d73a7e3c618c src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Fri Nov 05 20:42:06 2021 +0100 +++ b/src/Pure/Thy/html.scala Fri Nov 05 22:43:29 2021 +0100 @@ -376,13 +376,21 @@ /* fonts */ + val fonts_path: Path = Path.explode("fonts") + + def init_fonts(dir: Path): Unit = + { + val fonts_dir = Isabelle_System.make_directory(dir + HTML.fonts_path) + for (entry <- Isabelle_Fonts.fonts(hidden = true)) + Isabelle_System.copy_file(entry.path, fonts_dir) + } + + def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name + def fonts_url(): String => String = (for (entry <- Isabelle_Fonts.fonts(hidden = true)) yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap - def fonts_dir(prefix: String)(ttf_name: String): String = - prefix + "/" + ttf_name - def fonts_css(make_url: String => String = fonts_url()): String = { def font_face(entry: Isabelle_Fonts.Entry): String = @@ -399,26 +407,33 @@ .mkString("", "\n\n", "\n") } + def fonts_css_dir(prefix: String = ""): String = + { + val prefix1 = if (prefix.isEmpty || prefix.endsWith("/")) prefix else prefix + "/" + fonts_css(fonts_dir(prefix1 + fonts_path.implode)) + } - /* document directory */ + + /* document directory context (fonts + css) */ + + def relative_prefix(dir: Path, base: Option[Path]): String = + base match { + case None => "" + case Some(base_dir) => + File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile).implode + } def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") - def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")): Unit = - { - File.write(dir + isabelle_css.base, - fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) - } - - def init_dir(dir: Path): Unit = - write_isabelle_css(Isabelle_System.make_directory(dir)) - def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, + base: Option[Path] = None, css: String = isabelle_css.file_name, hidden: Boolean = true, structural: Boolean = true): Unit = { - init_dir(dir) + 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)) File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden, structural = structural)) } diff -r b2df121ccfc1 -r d73a7e3c618c src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Nov 05 20:42:06 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Fri Nov 05 22:43:29 2021 +0100 @@ -18,14 +18,11 @@ /* HTML context */ - val fonts_path = Path.explode("fonts") - sealed case class HTML_Document(title: String, content: String) - def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context = - new HTML_Context(fonts_url) + def html_context(): HTML_Context = new HTML_Context - final class HTML_Context private[Presentation](fonts_url: String => String) + final class HTML_Context private[Presentation] { val term_cache: Term.Cache = Term.Cache.make() @@ -44,13 +41,6 @@ }) } - def init_fonts(dir: Path): Unit = - { - val fonts_dir = Isabelle_System.make_directory(dir + fonts_path) - for (entry <- Isabelle_Fonts.fonts(hidden = true)) - Isabelle_System.copy_file(entry.path, fonts_dir) - } - def head(title: String, rest: XML.Body = Nil): XML.Tree = HTML.div("head", HTML.chapter(title) :: rest) @@ -66,15 +56,16 @@ else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items)))) } - def output_document(title: String, body: XML.Body): String = - HTML.output_document( - List( - HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), - HTML.title(title)), - List(HTML.source(body)), css = "", structural = false) - - def html_document(title: String, body: XML.Body): HTML_Document = - HTML_Document(title, output_document(title, body)) + def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document = + { + val content = + HTML.output_document( + List( + HTML.style(fonts_css + "\n\n" + File.read(HTML.isabelle_css)), + HTML.title(title)), + List(HTML.source(body)), css = "", structural = false) + HTML_Document(title, content) + } } @@ -202,7 +193,8 @@ snapshot: Document.Snapshot, html_context: HTML_Context, elements: Elements, - plain_text: Boolean = false): HTML_Document = + plain_text: Boolean = false, + fonts_css: String = HTML.fonts_css()): HTML_Document = { require(!snapshot.is_outdated, "document snapshot outdated") @@ -210,7 +202,7 @@ if (plain_text) { val title = "File " + Symbol.cartouche_decoded(name.path.file_name) val body = HTML.text(snapshot.node.source) - html_context.html_document(title, body) + html_context.html_document(title, body, fonts_css) } else { resources.html_document(snapshot) getOrElse { @@ -219,7 +211,7 @@ else "File " + Symbol.cartouche_decoded(name.path.file_name) val xml = snapshot.xml_markup(elements = elements.html) val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml) - html_context.html_document(title, body) + html_context.html_document(title, body, fonts_css) } } } @@ -269,7 +261,7 @@ else Nil } - def update_chapter_index( + def update_chapter( presentation_dir: Path, chapter: String, new_sessions: List[(String, String)]): Unit = { val dir = Isabelle_System.make_directory(presentation_dir + Path.basic(chapter)) @@ -297,12 +289,14 @@ val descr = Symbol.trim_blank_lines(description) (List(HTML.link(name + "/index.html", HTML.text(name))), if (descr == "") Nil - else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) + else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))), + base = Some(presentation_dir)) } - def update_global_index(presentation_dir: Path): Unit = + def update_root(presentation_dir: Path): Unit = { Isabelle_System.make_directory(presentation_dir) + HTML.init_fonts(presentation_dir) Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), presentation_dir + Path.explode("isabelle.gif")) val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" @@ -393,9 +387,8 @@ val options = info.options val base = deps(session) - val session_dir = presentation.dir(db_context.store, info) - - html_context.init_fonts(session_dir) + val presentation_dir = presentation.dir(db_context.store) + val session_dir = Isabelle_System.make_directory(presentation.dir(db_context.store, info)) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) @@ -571,11 +564,10 @@ } val file_path = session_dir + Path.explode(file_name) - html_context.init_fonts(file_path.dir) - val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) HTML.write_document(file_path.dir, file_path.file_name, - List(HTML.title(file_title)), List(html_context.head(file_title), file_html)) + List(HTML.title(file_title)), List(html_context.head(file_title), file_html), + base = Some(presentation_dir)) List(HTML.link(file_name, HTML.text(file_title))) } @@ -583,7 +575,8 @@ val thy_title = "Theory " + thy.name.theory_base_name HTML.write_document(session_dir, html_name(thy.name), - List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html)) + List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html), + base = Some(presentation_dir)) List(HTML.link(html_name(thy.name), HTML.text(thy.name.theory_base_name) ::: @@ -595,6 +588,7 @@ HTML.write_document(session_dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), html_context.head(title, List(HTML.par(view_links))) :: - html_context.contents("Theories", theories)) + html_context.contents("Theories", theories), + base = Some(presentation_dir)) } } diff -r b2df121ccfc1 -r d73a7e3c618c src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Nov 05 20:42:06 2021 +0100 +++ b/src/Pure/Tools/build.scala Fri Nov 05 22:43:29 2021 +0100 @@ -499,11 +499,11 @@ if (presentation_sessions.nonEmpty) { val presentation_dir = presentation.dir(store) progress.echo("Presentation in " + presentation_dir.absolute) - Presentation.update_global_index(presentation_dir) + Presentation.update_root(presentation_dir) for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) { val entries = infos.map(info => (info.name, info.description)) - Presentation.update_chapter_index(presentation_dir, chapter, entries) + Presentation.update_chapter(presentation_dir, chapter, entries) } val resources = Resources.empty diff -r b2df121ccfc1 -r d73a7e3c618c src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Nov 05 20:42:06 2021 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Fri Nov 05 22:43:29 2021 +0100 @@ -324,11 +324,12 @@ } yield { val snapshot = model.await_stable_snapshot() - val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root)) + val html_context = Presentation.html_context() val document = Presentation.html_document( PIDE.resources, snapshot, html_context, Presentation.elements2, - plain_text = query.startsWith(plain_text_prefix)) + plain_text = query.startsWith(plain_text_prefix), + fonts_css = HTML.fonts_css_dir(http_root)) HTTP.Response.html(document.content) })