# HG changeset patch
# User wenzelm
# Date 1636732168 -3600
# Node ID 32c2587cda4f069c2b57b95072fc00f646f05e26
# Parent  5d84f0312a3ac549352a83ee88df5a1df2e074b2
clarified HTML_Context: more explicit directory structure;

diff -r 5d84f0312a3a -r 32c2587cda4f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 12 14:37:00 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 12 16:49:28 2021 +0100
@@ -20,8 +20,21 @@
 
   sealed case class HTML_Document(title: String, content: String)
 
-  class HTML_Context
+  abstract class HTML_Context
   {
+    /* directory structure */
+
+    def root_dir: Path
+    def theory_session(name: Document.Node.Name): Sessions.Info
+
+    def session_dir(info: Sessions.Info): Path =
+      root_dir + Path.explode(info.chapter_session)
+    def theory_path(name: Document.Node.Name): Path =
+      session_dir(theory_session(name)) + Path.explode(name.theory_base_name).html
+    def files_path(name: Document.Node.Name, path: Path): Path =
+      theory_path(name).dir + Path.explode("files") + path.squash.html
+
+
     /* cached theory exports */
 
     val cache: Term.Cache = Term.Cache.make()
@@ -437,13 +450,12 @@
 
   val session_graph_path = Path.explode("session_graph.pdf")
   val readme_path = Path.explode("README.html")
-  val files_path = Path.explode("files")
 
   def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
-  def html_path(path: Path): String = (files_path + path.squash.html).implode
+  def files_path(src_path: Path): String = (Path.explode("files") + src_path.squash.html).implode
 
-  private def node_file(node: Document.Node.Name): String =
-    if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+  private def node_file(name: Document.Node.Name): String =
+    if (name.node.endsWith(".thy")) html_name(name) else files_path(name.path)
 
   private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
   {
@@ -482,20 +494,14 @@
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
-    session_elements: Elements,
-    presentation: Context): Unit =
+    session_elements: Elements): Unit =
   {
     val hierarchy = deps.sessions_structure.hierarchy(session)
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
 
-    def make_session_dir(name: String): Path =
-      Isabelle_System.make_directory(
-        presentation.dir(db_context.store, deps.sessions_structure(name)))
-
-    val session_dir = make_session_dir(session)
-    val presentation_dir = presentation.dir(db_context.store)
+    val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
 
     Bytes.write(session_dir + session_graph_path,
       graphview.Graph_File.make_pdf(options, base.session_graph_display))
@@ -560,10 +566,15 @@
     val theories: List[XML.Body] =
     {
       sealed case class Seen_File(
-        src_path: Path, file_name: String, thy_session: String, thy_name: Document.Node.Name)
+        src_path: Path, thy_name: Document.Node.Name, thy_session: String)
       {
-        def check(src_path1: Path, file_name1: String, thy_session1: String): Boolean =
-          (src_path == src_path1 || file_name == file_name1) && thy_session == thy_session1
+        val files_path: Path = html_context.files_path(thy_name, src_path)
+
+        def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean =
+        {
+          val files_path1 = html_context.files_path(thy_name1, src_path1)
+          (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1
+        }
       }
       var seen_files = List.empty[Seen_File]
 
@@ -609,36 +620,34 @@
       }
 
       (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
-        val thy_session = base.theory_qualifier(thy.name)
-        val thy_dir = make_session_dir(thy_session)
+        val thy_session = html_context.theory_session(thy.name)
+        val thy_dir = Isabelle_System.make_directory(html_context.session_dir(thy_session))
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
-            val file_name = html_path(src_path)
-
-            seen_files.find(_.check(src_path, file_name, thy_session)) match {
-              case None => seen_files ::= Seen_File(src_path, file_name, thy_session, thy.name)
+            seen_files.find(_.check(src_path, thy.name, thy_session.name)) match {
+              case None => seen_files ::= Seen_File(src_path, thy.name, thy_session.name)
               case Some(seen_file) =>
-                error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
+                error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
                   " in theory " + seen_file.thy_name + " vs. " + thy.name)
             }
 
-            val file_path = thy_dir + Path.explode(file_name)
+            val file_path = html_context.files_path(thy.name, src_path)
             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),
-              base = Some(presentation_dir))
+              base = Some(html_context.root_dir))
 
-            List(HTML.link(file_name, HTML.text(file_title)))
+            List(HTML.link(files_path(src_path), HTML.text(file_title)))
           }
 
         val thy_title = "Theory " + thy.name.theory_base_name
 
         HTML.write_document(thy_dir, html_name(thy.name),
           List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html),
-          base = Some(presentation_dir))
+          base = Some(html_context.root_dir))
 
-        if (thy_session == session) {
+        if (thy_session.name == session) {
           Some(
             List(HTML.link(html_name(thy.name),
               HTML.text(thy.name.theory_base_name) :::
@@ -653,6 +662,6 @@
       List(HTML.title(title + Isabelle_System.isabelle_heading())),
       html_context.head(title, List(HTML.par(view_links))) ::
         html_context.contents("Theories", theories),
-      base = Some(presentation_dir))
+      base = Some(html_context.root_dir))
   }
 }
diff -r 5d84f0312a3a -r 32c2587cda4f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Nov 12 14:37:00 2021 +0100
+++ b/src/Pure/Tools/build.scala	Fri Nov 12 16:49:28 2021 +0100
@@ -506,17 +506,22 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        val html_context =
-          new Presentation.HTML_Context { override val cache: Term.Cache = store.cache }
-
         using(store.open_database_context())(db_context =>
-          for (info <- presentation_sessions) {
+          for (session <- presentation_sessions.map(_.name)) {
             progress.expose_interrupt()
-            progress.echo("Presenting " + info.name + " ...")
+            progress.echo("Presenting " + session + " ...")
+
+            val html_context =
+              new Presentation.HTML_Context {
+                override val cache: Term.Cache = store.cache
+                override def root_dir: Path = presentation_dir
+                override def theory_session(name: Document.Node.Name): Sessions.Info =
+                  deps.sessions_structure(deps(session).theory_qualifier(name))
+              }
             Presentation.session_html(
-              info.name, deps, db_context, progress = progress,
+              session, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
-              Presentation.elements1, presentation = presentation)
+              Presentation.elements1)
           })
       }
     }
diff -r 5d84f0312a3a -r 32c2587cda4f src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Nov 12 14:37:00 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Nov 12 16:49:28 2021 +0100
@@ -31,7 +31,12 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val html_context = new Presentation.HTML_Context
+                  val html_context =
+                    new Presentation.HTML_Context {
+                      override def root_dir: Path = Path.current
+                      override def theory_session(name: Document.Node.Name): Sessions.Info =
+                        resources.sessions_structure(resources.session_base.theory_qualifier(name))
+                    }
                   val document =
                     Presentation.html_document(snapshot, html_context, Presentation.elements2)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
diff -r 5d84f0312a3a -r 32c2587cda4f src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Nov 12 14:37:00 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Nov 12 16:49:28 2021 +0100
@@ -324,7 +324,13 @@
         }
         yield {
           val snapshot = model.await_stable_snapshot()
-          val html_context = new Presentation.HTML_Context
+          val html_context =
+            new Presentation.HTML_Context {
+              override def root_dir: Path = Path.current
+              override def theory_session(name: Document.Node.Name): Sessions.Info =
+                PIDE.resources.sessions_structure(
+                  PIDE.resources.session_base.theory_qualifier(name))
+            }
           val document =
             Presentation.html_document(
               snapshot, html_context, Presentation.elements2,