# HG changeset patch # User clasohm # Date 814711984 -3600 # Node ID 9fb65f3db3198746c51a29a4cb1403fdc5154a7d # Parent 0c0e6298df138e54d83a873849e2f212cbff168c renamed chart00 and 00-chart to "index" diff -r 0c0e6298df13 -r 9fb65f3db319 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Thu Oct 26 13:53:00 1995 +0100 +++ b/src/Pure/Thy/ROOT.ML Thu Oct 26 13:53:04 1995 +0100 @@ -38,7 +38,7 @@ \and ThmDB = ThmDB);", "ReadThy.loaded_thys := !loaded_thys;", "ReadThy.gif_path := !gif_path;", - "ReadThy.chart00_path := !chart00_path;", + "ReadThy.index_path := !index_path;", "ReadThy.make_html := !make_html;", "ThmDB.thm_db := !thm_db;", "open ThmDB ReadThy;"]; diff -r 0c0e6298df13 -r 9fb65f3db319 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Thu Oct 26 13:53:00 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Thu Oct 26 13:53:04 1995 +0100 @@ -68,7 +68,7 @@ val print_theory: theory -> unit val gif_path : string ref - val chart00_path : string ref + val index_path : string ref val make_html : bool ref val init_html: unit -> unit val make_chart: unit -> unit @@ -120,8 +120,8 @@ space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))) "Tools"); -(*Location of theory-list.txt and 00-chart.html (normally set by init_html)*) -val chart00_path = ref ""; +(*Location of theory-list.txt and index.html (normally set by init_html)*) +val index_path = ref ""; val make_html = ref false; (*don't make HTML versions of loaded theories*) @@ -307,9 +307,9 @@ (sup if this head is for a sub-chart, sub if it is for a sup-chart; empty for Pure and CPure sub-charts) gif_path: relative path to directory containing GIFs - chart00_path: relative path to directory containing main theory chart + index_path: relative path to directory containing main theory chart *) -fun mk_charthead file tname title green_arrow gif_path chart00_path package = +fun mk_charthead file tname title green_arrow gif_path index_path package = output (file, "" ^ title ^ " of " ^ tname ^ "\n

" ^ title ^ " of theory " ^ tname ^ @@ -321,15 +321,15 @@ (if not green_arrow then "" else "
> stands for repeated subtrees") ^ - "

Back to the main theory chart of " ^ package ^ ".\n

\n
");
 
 (*Convert .thy file to HTML and make chart of its super-theories*)
 fun thyfile2html tpath tname =
   let
     val gif_path = relative_path tpath (!gif_path);
-    val package = hd (rev (space_explode "/" (!chart00_path)));
-    val chart00_path = relative_path tpath (!chart00_path);
+    val package = hd (rev (space_explode "/" (!index_path)));
+    val index_path = relative_path tpath (!index_path);
 
     (*Make list of all theories and all theories that own a .thy file*)
     fun list_theories [] theories thy_files = (theories, thy_files)
@@ -404,7 +404,7 @@
           in (implode pre ^ ancestors, body) end;
       in "" ^ tname ^ ".thy\n\n\n" ^
          "
" ^ tname ^ ".thy
\nBack to the main theory chart of " ^ package ^
          ".\n
\n\n
\n" ^ comment ^ ancestors ^ body ^
          "
\n
Theorems proved in " ^ tname ^ " \
        \
");
      close_out sup_out;
 
-     mk_charthead sub_out tname "Children" false gif_path chart00_path package;
+     mk_charthead sub_out tname "Children" false gif_path index_path package;
      output(sub_out,
        "" ^ tname ^ " \
        \Isabelle/" ^ subdir ^ "\n\
        \
Isabelle/" ^ subdir ^ "
\n\
@@ -1069,7 +1069,7 @@
        \/\\ stands for supertheories (parent theories)\n\
        \
\
+       tack_on (relative_path (!index_path) base_path) "index.html\">\
        \Back to the index of Isabelle logics.\n
" ^
        main_entries theories (space_explode "/" base_path) ^
        "\n");