present auxiliary files with PIDE markup;
more robust treatment of non-text files (notably $POLYML_EXE);

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

--- 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 */
 

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

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

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

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

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

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

--- 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())