clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
authorwenzelm
Fri, 19 Aug 2022 21:43:06 +0200
changeset 75915 95d7459e5bc0
parent 75914 4da80799352f
child 75916 b6589c8ccadd
clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;
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 {