# HG changeset patch
# User clasohm
# Date 815746504 -3600
# Node ID ae24fa2492669949bd30b80b14c2fd2a080eacad
# Parent  9b3d3362a0481c716393e7952f352aca7a40ab29
added leading "." to HTML filenames

diff -r 9b3d3362a048 -r ae24fa249266 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Tue Nov 07 12:58:17 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Tue Nov 07 13:15:04 1995 +0100
@@ -389,7 +389,7 @@
                   fun make_link t =
                     let val path = path_of t;
                     in "<A HREF = \"" ^
-                       tack_on (relative_path tpath path) t ^
+                       tack_on (relative_path tpath path) ("." ^ t) ^
                        ".html\">" ^ t ^ "</A>" end;
               in if not (id mem theories) then (result, implode l)
                  else if id mem thy_files then
@@ -417,8 +417,8 @@
 
     (** Make chart of super-theories **)
 
-    val sup_out = open_out (tack_on tpath tname ^ "_sup.html");
-    val sub_out = open_out (tack_on tpath tname ^ "_sub.html");
+    val sup_out = open_out (tack_on tpath ("." ^ tname ^ "_sup.html"));
+    val sub_out = open_out (tack_on tpath ("." ^ tname ^ "_sub.html"));
 
     (*Theories that already have been listed in this chart*)
     val listed = ref [];
@@ -447,14 +447,15 @@
                     mk_offset ls (l+1);
             in output (sup_out,
                  " " ^ mk_offset continued 0 ^
-                 "\\__" ^ (if is_pure then t else "<A HREF=\"" ^ 
-                             tack_on rel_path t ^ ".html\">" ^ t ^ "</A>") ^
+                 "\\__" ^ (if is_pure then t else
+                             "<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^
+                             ".html\">" ^ t ^ "</A>") ^
                  (if repeated then "..." else " ") ^
-                 "<A HREF = \"" ^ tack_on rel_path t ^
+                 "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^
                  "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
                  tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
                  (if is_pure then ""
-                  else "<A HREF = \"" ^ tack_on rel_path t ^
+                  else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^
                        "_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
                        tack_on gif_path "blue_arrow.gif\
                        \\" ALT = /\\></A>") ^
@@ -470,15 +471,15 @@
           filter (fn s => s mem wanted_theories) (parents_of tname);
       in mk_entry relatives end;
   in if is_some (!cur_htmlfile) then
-       error "thyfile2html: Last theory's HTML has not been closed."
+       error "thyfile2html: Last theory's HTML file has not been closed."
      else ();
-     cur_htmlfile := Some (open_out (tack_on tpath tname ^ ".html"));
+     cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
      output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
 
      mk_charthead sup_out tname "Ancestors" true gif_path index_path package;
      output(sup_out,
-       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
-       \<A HREF = \"" ^ tname ^
+       "<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
+       \<A HREF = \"." ^ tname ^
        "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
        tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n");
      list_ancestors tname 0 [];
@@ -487,8 +488,8 @@
 
      mk_charthead sub_out tname "Children" false gif_path index_path package;
      output(sub_out,
-       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
-       \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
+       "<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
+       \<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
        tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
      close_out sub_out
   end;
@@ -595,22 +596,23 @@
 
                val gif_path = relative_path path (!gif_path);
                val rel_path = relative_path path abs_path;
+               val tpath = tack_on rel_path ("." ^ tname);
 
-               val out = open_append (tack_on path t ^ "_sub.html");
+               val out = open_append (tack_on path ("." ^ t ^ "_sub.html"));
            in output (out,
-                " |\n \\__<A HREF=\"" ^ tack_on rel_path tname ^ ".html\">" ^
-                tname ^ "</A> <A HREF = \"" ^
-                tack_on rel_path tname ^
-                "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+                " |\n \\__<A HREF=\"" ^
+                tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^
+                "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
+                \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
                 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\
-                \<A HREF = \"" ^ tack_on rel_path tname ^ "_sup.html\">\
+                \<A HREF = \"" ^ tpath ^ "_sup.html\">\
                 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
                 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
               close_out out
            end;
 
          val theory_list =
-           open_append (tack_on (!index_path) "theory_list.txt");
+           open_append (tack_on (!index_path) ".theory_list.txt");
      in output (theory_list, tname ^ " " ^ abs_path ^ "\n");
         close_out theory_list;
 
@@ -998,9 +1000,9 @@
 
 (*Init HTML generator by setting paths and creating new files*)
 fun init_html () =
-  let val pure_out = open_out "Pure_sub.html";
-      val cpure_out = open_out "CPure_sub.html";
-      val theory_list = close_out (open_out "theory_list.txt");
+  let val pure_out = open_out ".Pure_sub.html";
+      val cpure_out = open_out ".CPure_sub.html";
+      val theory_list = close_out (open_out ".theory_list.txt");
 
       val rel_gif_path = relative_path (pwd ()) (!gif_path);
       val package = hd (rev (space_explode "/" (pwd ())));
@@ -1019,7 +1021,7 @@
 
 (*Generate index.html*)
 fun make_chart () = if not (!make_html) then () else
-  let val theory_list = open_in (tack_on (!index_path) "theory_list.txt");
+  let val theory_list = open_in (tack_on (!index_path) ".theory_list.txt");
       val theories = space_explode "\n" (input (theory_list, 999999));
       val dummy = close_in theory_list;
 
@@ -1039,7 +1041,7 @@
               val tname = implode name
               val tpath =
                 tack_on (relative_path (!index_path) (implode (tl path)))
-                        tname;
+                        ("." ^ tname);
               val subdir = space_explode "/"
                                  (relative_path base_path (implode (tl path)));
               val level_diff = length subdir - length curdir;