# HG changeset patch
# User berghofe
# Date 875616834 -7200
# Node ID e5d2399a154fe9e5d8f3739a39a733ace34e7fed
# Parent cd9b6c86926c5e2afb41ca8cd94e2d35959bb0ce
Changed html data directory and names of graph files.
diff -r cd9b6c86926c -r e5d2399a154f src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML Tue Sep 30 12:52:15 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML Tue Sep 30 12:53:54 1997 +0200
@@ -88,12 +88,13 @@
corresponding to theory with given path *)
local
fun make_path q p =
- let val base = tack_on (normalize_path (!output_dir)) q;
+ let val outp_dir = normalize_path (!output_dir);
+ val base = if q = "" then outp_dir else tack_on outp_dir q;
val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
else relative_path (normalize_path (!home_path)) p;
in tack_on base rpath end
in
- val html_path = make_path "html";
+ val html_path = make_path "";
val graph_path = make_path "graph/data"
end;
@@ -544,7 +545,7 @@
not contain the string "Isabelle/"*)
val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
val rel_graph_path = tack_on (relative_path (!index_path) (graph_path (!original_path)))
- "theories.html"
+ "small.html"
in TextIO.output (out,
"" ^ title ^ "\n\
\" ^ title ^ "
\n\
@@ -680,24 +681,24 @@
val rel_index_path = tack_on (relative_path
abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html";
val outfile =
- tack_on abs_path ((if large then "all_" else "") ^ "theories.html");
+ tack_on abs_path ((if large then "large" else "small") ^ ".html");
val os = TextIO.openOut outfile;
val _ = TextIO.output(os,
"" ^ dir_name ^ "\n\
\" ^ dir_name ^ "
\n" ^
(if other_graph then
(if large then
- "View small graph without \
+ "View small graph without \
\subdirectories\n"
else
- "View large graph including \
+ "View large graph including \
\all subdirectories
\n")
else "") ^
"Back to index\n
\n\
\\n
\n")
val _ = TextIO.closeOut os
in () end;
@@ -709,11 +710,11 @@
base_path := normalize_path (!base_path);
mkdir gpath;
original_path := pwd ();
- graph_file := tack_on gpath "theories.graph";
+ graph_file := tack_on gpath "small.graph";
graph_root_dir := (if usedir_arg = "." then pwd ()
else normalize_path (tack_on (pwd ()) ".."));
(if (!graph_base_file) = "" then
- (large_graph_file := tack_on gpath "all_theories.graph";
+ (large_graph_file := tack_on gpath "large.graph";
default_graph (!graph_file);
default_graph (!large_graph_file);
mk_applet_page gpath false true;
@@ -725,7 +726,7 @@
(copy_graph (!graph_base_file) (!graph_file) true;
mk_applet_page gpath false false)
else
- (large_graph_file := tack_on gpath "all_theories.graph";
+ (large_graph_file := tack_on gpath "large.graph";
mk_applet_page gpath false true;
mk_applet_page gpath true true;
copy_graph (!graph_base_file) (!graph_file) false;