# HG changeset patch # User wenzelm # Date 1608475674 -3600 # Node ID af2d0e07493b5281dd46a0a1ba1fcc3cac69593f # Parent f78730341c87b9e67fa8a1de85075402aced60b4 present auxiliary files with PIDE markup; more robust treatment of non-text files (notably $POLYML_EXE); diff -r f78730341c87 -r af2d0e07493b etc/isabelle.css --- a/etc/isabelle.css Sun Dec 20 13:20:09 2020 +0100 +++ b/etc/isabelle.css Sun Dec 20 15:47:54 2020 +0100 @@ -20,7 +20,7 @@ font-family: "Isabelle DejaVu Sans Mono", monospace; } -.theories { background-color: #FFFFFF; padding: 10px; } +.contents { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } .document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; } diff -r f78730341c87 -r af2d0e07493b src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/General/path.scala Sun Dec 20 15:47:54 2020 +0100 @@ -67,6 +67,15 @@ case Parent => ".." } + private def squash_elem(elem: Elem): String = + elem match { + case Root("") => "ROOT" + case Root(s) => "SERVER_" + s + case Basic(s) => s + case Variable(s) => s + case Parent => "PARENT" + } + /* path constructors */ @@ -201,6 +210,7 @@ } def xz: Path = ext("xz") + def html: Path = ext("html") def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") @@ -234,6 +244,8 @@ def drop_ext: Path = split_ext._1 def get_ext: String = split_ext._2 + def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem)))) + /* expand */ diff -r f78730341c87 -r af2d0e07493b src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/PIDE/command.scala Sun Dec 20 15:47:54 2020 +0100 @@ -30,7 +30,7 @@ src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) { - def read_file: String = File.read(name.path) + def read_file: Bytes = Bytes.read(name.path) def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) diff -r f78730341c87 -r af2d0e07493b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/PIDE/document.scala Sun Dec 20 15:47:54 2020 +0100 @@ -620,16 +620,23 @@ elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) - def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] = + def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full) + : List[(Path, XML.Body)] = { snippet_command match { case None => Nil case Some(command) => for (Exn.Res(blob) <- command.blobs) yield { - val text = blob.read_file - val markup = command.init_markups(Command.Markup_Index.blob(blob)) - markup.to_XML(Text.Range(0, text.length), text, elements) + val bytes = blob.read_file + val text = bytes.text + val xml = + if (Bytes(text) == bytes) { + val markup = command.init_markups(Command.Markup_Index.blob(blob)) + markup.to_XML(Text.Range(0, text.length), text, elements) + } + else Nil + blob.src_path -> xml } } } diff -r f78730341c87 -r af2d0e07493b src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Dec 20 15:47:54 2020 +0100 @@ -12,6 +12,12 @@ import java.io.{File => JFile} +object Resources +{ + def empty: Resources = + new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) +} + class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, diff -r f78730341c87 -r af2d0e07493b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/ROOT.ML Sun Dec 20 15:47:54 2020 +0100 @@ -354,4 +354,3 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" - diff -r f78730341c87 -r af2d0e07493b src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/Thy/presentation.scala Sun Dec 20 15:47:54 2020 +0100 @@ -14,6 +14,8 @@ { /** HTML documents **/ + 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 = @@ -21,6 +23,25 @@ final class HTML_Context private[Presentation](fonts_url: String => String) { + def init_fonts(dir: Path) + { + val fonts_dir = Isabelle_System.make_directory(dir + fonts_path) + for (entry <- Isabelle_Fonts.fonts(hidden = true)) + File.copy(entry.path, fonts_dir) + } + + def head(title: String, rest: XML.Body = Nil): XML.Tree = + HTML.div("head", HTML.chapter(title) :: rest) + + def source(body: XML.Body): XML.Tree = HTML.pre("source", body) + + def contents(heading: String, items: List[XML.Body], css_class: String = "contents") + : List[XML.Elem] = + { + if (items.isEmpty) Nil + 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( @@ -86,26 +107,24 @@ def html_document( resources: Resources, snapshot: Document.Snapshot, - context: HTML_Context, + html_context: HTML_Context, plain_text: Boolean = false): HTML_Document = { require(!snapshot.is_outdated) val name = snapshot.node_name if (plain_text) { - val title = "File " + quote(name.path.file_name) + val title = "File " + Symbol.cartouche_decoded(name.path.file_name) val body = HTML.text(snapshot.node.source) - context.html_document(title, body) + html_context.html_document(title, body) } else { - resources.html_document(snapshot) match { - case Some(document) => document - case None => - val title = - if (name.is_theory) "Theory " + quote(name.theory_base_name) - else "File " + quote(name.path.file_name) - val body = html_body(snapshot.xml_markup(elements = html_elements)) - context.html_document(title, body) + resources.html_document(snapshot) getOrElse { + val title = + if (name.is_theory) "Theory " + quote(name.theory_base_name) + else "File " + Symbol.cartouche_decoded(name.path.file_name) + val body = html_body(snapshot.xml_markup(elements = html_elements)) + html_context.html_document(title, body) } } } @@ -352,9 +371,11 @@ } def session_html( + resources: Resources, session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, + html_context: HTML_Context, presentation: Context) { val info = deps.sessions_structure(session) @@ -362,9 +383,8 @@ val base = deps(session) val session_dir = presentation.dir(db_context.store, info) - val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts")) - for (entry <- Isabelle_Fonts.fonts(hidden = true)) - File.copy(entry.path, session_fonts) + + html_context.init_fonts(session_dir) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) @@ -406,6 +426,39 @@ HTML.link(prefix + html_name(name1), body) } + val files: List[XML.Body] = + { + var seen_files = List.empty[(Path, String, Document.Node.Name)] + (for { + thy_name <- base.session_theories.iterator + thy_command <- + Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator + snapshot = Document.State.init.snippet(thy_command) + (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator + if xml.nonEmpty + } yield { + val file_title = src_path.implode_short + val file_name = (files_path + src_path.squash.html).implode + + seen_files.find(p => p._1 == src_path || p._2 == file_name) match { + case None => seen_files ::= (src_path, file_name, thy_name) + case Some((_, _, thy_name1)) => + error("Incoherent use of file name " + src_path + " as " + quote(file_name) + + " in theory " + thy_name1 + " vs. " + thy_name) + } + + val file_path = session_dir + Path.explode(file_name) + html_context.init_fonts(file_path.dir) + + val title = "File " + Symbol.cartouche_decoded(file_title) + HTML.write_document(file_path.dir, file_path.file_name, + List(HTML.title(title)), + List(html_context.head(title), html_context.source(html_body(xml)))) + + List(HTML.link(file_name, HTML.text(file_title))) + }).toList + } + val theories = for (name <- base.session_theories) yield { @@ -440,7 +493,7 @@ val title = "Theory " + name.theory_base_name HTML.write_document(session_dir, html_name(name), List(HTML.title(title)), - HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body))) + List(html_context.head(title), html_context.source(thy_body))) List(HTML.link(html_name(name), HTML.text(name.theory_base_name))) } @@ -448,9 +501,9 @@ val title = "Session " + session HTML.write_document(session_dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), - HTML.div("head", List(HTML.chapter(title), HTML.par(links))) :: - (if (theories.isEmpty) Nil - else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories)))))) + html_context.head(title, List(HTML.par(links))) :: + html_context.contents("Theories", theories) ::: + html_context.contents("Files", files)) } diff -r f78730341c87 -r af2d0e07493b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/Tools/build.scala Sun Dec 20 15:47:54 2020 +0100 @@ -502,11 +502,15 @@ val presentation_dir = presentation.dir(store) progress.echo("Presentation in " + presentation_dir.absolute) + val resources = Resources.empty + val html_context = Presentation.html_context() + using(store.open_database_context())(db_context => for ((_, (session_name, _)) <- presentation_chapters) { progress.expose_interrupt() progress.echo("Presenting " + session_name + " ...") - Presentation.session_html(session_name, deps, db_context, presentation) + Presentation.session_html( + resources, session_name, deps, db_context, html_context, presentation) }) val browser_chapters = diff -r f78730341c87 -r af2d0e07493b src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Sun Dec 20 15:47:54 2020 +0100 @@ -94,7 +94,7 @@ { val store = Sessions.store(options) - val resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) + val resources = Resources.empty val session = new Session(options, resources) using(store.open_database_context())(db_context => @@ -376,7 +376,7 @@ export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) - for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) { + for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export(Export.MARKUP + (i + 1), xml) } export(Export.MARKUP, snapshot.xml_markup())