# HG changeset patch
# User wenzelm
# Date 1660935569 -7200
# Node ID 4d5221c51f8e9c5d086fbcf3cc918d06ccfa5d27
# Parent  ffec626541e2624e1abf8ac24b87fdb5b92091df
clarified directory layout: files are relative to enclosing theory;

diff -r ffec626541e2 -r 4d5221c51f8e src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 20:42:19 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 20:59:29 2022 +0200
@@ -44,11 +44,12 @@
     def theory_html(theory: Document_Info.Theory): Path =
       Path.explode(theory.print_short).html
 
-    def file_html(path: Path): Path =
-      Path.explode("files") + path.squash.html
+    def file_html(theory: Document_Info.Theory, file: Path): Path =
+      Path.explode(theory.print_short) + file.squash.html
 
-    def smart_html(theory: Document_Info.Theory, file: String): Path =
-      if (File.is_thy(file)) theory_html(theory) else file_html(Path.explode(file))
+    def smart_html(theory: Document_Info.Theory, file: Path): Path =
+      if (File.is_thy(file.file_name)) theory_html(theory)
+      else file_html(theory, file: Path)
 
     def relative_link(dir: Path, file: Path): String =
       try { File.path(dir.java_path.relativize(file.java_path).toFile).implode }
@@ -191,7 +192,7 @@
                 html_ref <- logical_ref(theory) orElse physical_ref(theory)
               }
               yield {
-                val html_path = session_dir + html_context.smart_html(theory, def_file)
+                val html_path = session_dir + html_context.smart_html(theory, Path.explode(def_file))
                 val html_link = html_context.relative_link(file_dir, html_path)
                 HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body))
               }
@@ -520,7 +521,7 @@
         val files =
           for {
             (src_path, file_html) <- files_html
-            file_path = session_dir + html_context.file_html(src_path)
+            file_path = session_dir + html_context.file_html(theory, src_path)
             rel_path <- File.relative_path(session_dir, file_path)
           }
           yield {