" ^ title ^ " of " ^ tname ^ "

# HG changeset patch # User clasohm # Date 815318160 -3600 # Node ID 83ce32aa4e9b713242a5b53d3b0c86fda41a5c8b # Parent ce35d42d21908aa721af8ffe44ff6f37552c17ac removed borders from images in charts; replaced green arrow by "..." diff -r ce35d42d2190 -r 83ce32aa4e9b src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Thu Nov 02 12:45:58 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Thu Nov 02 14:16:00 1995 +0100 @@ -309,7 +309,7 @@ gif_path: relative path to directory containing GIFs index_path: relative path to directory containing main theory chart *) -fun mk_charthead file tname title green_arrow gif_path index_path package = +fun mk_charthead file tname title repeats gif_path index_path package = output (file, "" ^ title ^ " of " ^ tname ^ "\n

" ^ title ^ " of theory " ^ tname ^ @@ -318,9 +318,8 @@ \\" ALT = \\/> stands for subtheories (child theories)
\n\ \ $/\\$ stands for supertheories (parent theories)\n" ^ - (if not green_arrow then "" else - "

stands for repeated subtrees") ^ + (if not repeats then "" else + "
... stands for repeated subtrees") ^ "

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

");
 
@@ -328,7 +327,12 @@
 fun thyfile2html tpath tname =
   let
     val gif_path = relative_path tpath (!gif_path);
-    val package = hd (rev (space_explode "/" (!index_path)));
+    val package =
+      case rev (space_explode "/" (!index_path)) of
+          x::xs => x
+        | _ => error "index_path is empty. \
+                     \Please use 'init_html()' instead of \
+                     \'make_html := true'";
     val index_path = relative_path tpath (!index_path);
 
     (*Make list of all theories and all theories that own a .thy file*)
@@ -433,6 +437,7 @@
               val path = path_of t;
               val rel_path = if is_pure then index_path
                              else relative_path tpath path;
+              val repeated = t mem (!listed) andalso not (null (parents_of t));
 
               fun mk_offset [] cur =
                     if level < cur then error "Error in mk_offset"
@@ -444,21 +449,18 @@
                  " " ^ mk_offset continued 0 ^
                  "\\__" ^ (if is_pure then t else "" ^ t ^ "") ^
-                 " " ^
                  (if is_pure then ""
                   else ""));
-              if t mem (!listed) andalso not (null (parents_of t)) then
-                output (sup_out,
-                  "\
-                  \\n")
-              else (output (sup_out, "\n");
-                    listed := t :: (!listed);
+                       \\" ALT = /\\>") ^
+                 "\n");
+              if repeated then ()
+              else (listed := t :: (!listed);
                     list_ancestors t (level+1) (if null ts then continued
                                                 else continued @ [level]);
                     mk_entry ts)
@@ -476,7 +478,8 @@
      mk_charthead sup_out tname "Ancestors" true gif_path index_path package;
      output(sup_out,
        "" ^ tname ^ " \
-       \\n");
      list_ancestors tname 0 [];
      output (sup_out, "

"); @@ -486,7 +489,7 @@ output(sub_out, "" ^ tname ^ " \ \ $\\/$ \n"); + tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/>\n"); close_out sub_out end; @@ -598,11 +601,11 @@ " |\n \\__" ^ tname ^ "

$\\/$ \ \\ - \ $/\\$ \n"); + \ $/\\$ \n"); close_out out end;