# HG changeset patch
# User wenzelm
# Date 1660938186 -7200
# Node ID 95d7459e5bc0edeb2bf367bc90950f1246d7e671
# Parent  4da80799352f4480df4a4b59fae5e01cea185d45
clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;

diff -r 4da80799352f -r 95d7459e5bc0 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 21:25:13 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 21:43:06 2022 +0200
@@ -44,12 +44,11 @@
     def theory_html(theory: Document_Info.Theory): Path =
       Path.explode(theory.print_short).html
 
-    def file_html(theory: Document_Info.Theory, file: String): Path =
-      Path.explode(theory.print_short) + Path.explode(file).squash.html
+    def file_html(file: String): Path =
+      Path.explode(file).squash.html
 
     def smart_html(theory: Document_Info.Theory, file: String): Path =
-      if (File.is_thy(file)) theory_html(theory)
-      else file_html(theory, file)
+      if (File.is_thy(file)) theory_html(theory) else file_html(file)
 
     def relative_link(dir: Path, file: Path): String =
       try { File.path(dir.java_path.relativize(file.java_path).toFile).implode }
@@ -521,7 +520,7 @@
         val files =
           for {
             (blob, file_html) <- blobs_html
-            file_path = session_dir + html_context.file_html(theory, blob.name.node)
+            file_path = session_dir + html_context.file_html(blob.name.node)
             rel_path <- File.relative_path(session_dir, file_path)
           }
           yield {