# HG changeset patch
# User clasohm
# Date 814542624 -3600
# Node ID ae31bb7774a7e1d5c9cfd00444b6b5f3d7ef41b2
# Parent  27c1e88a62b4510b7570296aa6543652e52b12d2
added calls of init_html and make_chart

diff -r 27c1e88a62b4 -r ae31bb7774a7 src/Cube/Makefile
--- a/src/Cube/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/Cube/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (Cube)			#
@@ -8,6 +9,8 @@
 #	make 
 #To make the system and test it on standard examples, type  
 #	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -25,8 +28,17 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Cube ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' | $(BIN)/Pure ;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/Cube;\
+		else echo 'open PolyML; exit_use"ROOT";' \
+		       | $(COMP) $(BIN)/Cube;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/Cube/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -17,4 +17,6 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val Cube_build_completed = ();	(*indicate successful build*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOL/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,4 +1,4 @@
-#  $Id$
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (FOL)			#
@@ -6,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type  
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type  
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -35,10 +37,18 @@
                 	exit 1; \
            	fi;\
 	case "$(COMP)" in \
-	poly*)	echo 'make_database"$(BIN)/FOL"; quit();'  \
-			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOL;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;;\
+	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
+		  | $(COMP) $(BIN)/Pure;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/FOL;\
+		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOL;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOL" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOL/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -72,5 +72,6 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val FOL_build_completed = ();	(*indicate successful build*)
-
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOL/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -37,4 +37,6 @@
 time_use_thy "ex/Nat2";
 time_use_thy "ex/List";
 
+make_chart ();   (*make HTML chart*)
+
 maketest"END: Root file for FOL examples";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOLP/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -6,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type  
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type  
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -30,8 +32,17 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOLP;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/FOLP;\
+		else echo 'open PolyML; exit_use"ROOT";' \
+		       | $(COMP) $(BIN)/FOLP;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOLP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -78,4 +78,6 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val FOLP_build_completed = ();	(*indicate successful build*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/FOLP/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -32,4 +32,6 @@
 time_use     "ex/prop.ML";
 time_use     "ex/quant.ML";
 
+make_chart ();   (*make HTML chart*)
+
 maketest"END: Root file for FOLP examples";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/AxClasses/Group/ROOT.ML
--- a/src/HOL/AxClasses/Group/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/AxClasses/Group/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -25,3 +25,5 @@
 
 use_thy "GroupDefs";
 use_thy "GroupInsts";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/AxClasses/Tutorial/ROOT.ML
--- a/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -33,3 +33,5 @@
 
 use_thy "Product";
 use_thy "ProductInsts";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -22,3 +22,5 @@
 time_use_thy "Properties";
 time_use_thy "Equiv";
 time_use_thy "Hoare";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/Integ/ROOT.ML
--- a/src/HOL/Integ/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/Integ/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -10,3 +10,5 @@
 
 loadpath := ["Integ"];
 time_use_thy "Integ";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/Lambda/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -19,4 +19,7 @@
 
 writeln"Root file for HOL/Lambda";
 loadpath := [".","Lambda"];
+
 time_use_thy "Eta";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (HOL)			#
@@ -5,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type  
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type  
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -36,9 +39,17 @@
            	fi;\
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
-			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
+		  | $(COMP) $(BIN)/Pure;\
+		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                  | $(COMP) $(BIN)/HOL;\
+		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml; exit 1;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -85,4 +85,6 @@
 init_pps ();
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val HOL_build_completed = ();   (*indicate successful build*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/Subst/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -30,4 +30,6 @@
 
 use_thy "Unifier";
 
+make_chart ();   (*make HTML chart*)
+
 writeln"END: Root file for Substitutions and Unification";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -30,4 +30,7 @@
 time_use_thy "Term";
 time_use_thy "Simult";
 time_use_thy "MT";
+
+make_chart ();   (*make HTML chart*)
+
 writeln "END: Root file for HOL examples";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/LCF/Makefile
--- a/src/LCF/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/LCF/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (LCF)			#
@@ -8,6 +9,8 @@
 #	make 
 #To make the system and test it on standard examples, type  
 #	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -24,8 +27,16 @@
 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/LCF;\
+		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' \
+                       | $(BIN)/FOL;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/LCF/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -17,4 +17,6 @@
 use"pair.ML";
 use"fix.ML";
 
+make_chart ();   (*make HTML chart*)
+
 val LCF_build_completed = ();	(*indicate successful build*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/Modal/Makefile
--- a/src/Modal/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/Modal/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (Modal)			#
@@ -5,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type 
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -25,8 +28,17 @@
 $(BIN)/Modal:   $(BIN)/LK  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Modal ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' | $(BIN)/LK;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/Modal;\
+		else echo 'open PolyML; exit_use"ROOT";' \
+		       | $(COMP) $(BIN)/Modal;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' \
+                       | $(BIN)/LK;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/Modal/ROOT.ML
--- a/src/Modal/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/Modal/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -78,6 +78,8 @@
 end;
 structure S43_Prover = Modal_ProverFun(MP_Rule);  
 
+make_chart ();   (*make HTML chart*)
+
 val Modal_build_completed = ();	(*indicate successful build*)
 
 (*printing functions are inherited from LK*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/Modal/ex/ROOT.ML
--- a/src/Modal/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/Modal/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -25,4 +25,6 @@
 time_use "ex/S4thms.ML";
 time_use "ex/S43thms.ML";
 
+make_chart ();   (*make HTML chart*)
+
 maketest"END: Root file for Modal examples";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/AC/ROOT.ML
--- a/src/ZF/AC/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/AC/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -40,4 +40,6 @@
 
 time_use_thy "AC/DC";
 
+make_chart ();   (*make HTML chart*)
+
 writeln"END: Root file for ZF/AC";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/Coind/ROOT.ML
--- a/src/ZF/Coind/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/Coind/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -19,3 +19,5 @@
 proof_timing := true;
 loadpath     := [".","Coind"];
 time_use_thy "MT";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/IMP/ROOT.ML
--- a/src/ZF/IMP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/IMP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -18,3 +18,5 @@
 proof_timing := true;
 loadpath := [".","IMP"];
 time_use_thy "Equiv";
+
+make_chart ();   (*make HTML chart*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/Makefile	Tue Oct 24 14:50:24 1995 +0100
@@ -1,4 +1,4 @@
-#  $Id$
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (ZF)			#
@@ -6,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type 
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -35,8 +37,16 @@
 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/ZF;\
+		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' \
+                       | $(BIN)/FOL;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml; exit 1;;\
 	esac
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -40,4 +40,6 @@
 (*printing functions are inherited from FOL*)
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val ZF_build_completed = ();	(*indicate successful build*)
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/Resid/ROOT.ML
--- a/src/ZF/Resid/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/Resid/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -21,4 +21,6 @@
 
 time_use_thy "Confluence";
 
+make_chart ();   (*make HTML chart*)
+
 writeln"END: Root file for ZF/Resid";
diff -r 27c1e88a62b4 -r ae31bb7774a7 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
+++ b/src/ZF/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
@@ -42,4 +42,6 @@
 time_use_thy "ex/LList";
 time_use_thy "ex/CoUnit";
 
+make_chart ();   (*make HTML chart*)
+
 writeln"END: Root file for ZF Set Theory examples";