# HG changeset patch
# User clasohm
# Date 816963012 -3600
# Node ID 90d615b599d958e9fc7eb1b3d7f70b540e2db426
# Parent  6bdee79ef125d668f74a4bc137dc1792edb12bee
main directory is now read by exit_use_dir, too;
removed make_chart from ROOT.ML

diff -r 6bdee79ef125 -r 90d615b599d9 src/CCL/Makefile
--- a/src/CCL/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CCL/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -37,13 +37,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CCL;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CCL;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/CCL;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CCL" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/CCL/ROOT.ML
--- a/src/CCL/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CCL/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val CCL_build_completed = ();   (*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/CTT/Makefile
--- a/src/CTT/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CTT/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -36,13 +36,14 @@
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CTT;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/CTT;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CTT/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -23,6 +23,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val CTT_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/Cube/Makefile
--- a/src/Cube/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Cube/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,14 +29,14 @@
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Cube;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Cube/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -17,6 +17,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val Cube_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/FOLP/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -33,14 +33,14 @@
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOLP;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/FOLP/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -78,6 +78,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val FOLP_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/HOLCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -37,14 +37,14 @@
 	case "$(COMP)" in \
 	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOLCF;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/HOLCF;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
                        | $(BIN)/HOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/HOLCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 
 print_depth 100;  
 
-make_chart ();   (*make HTML chart*)
-
 val HOLCF_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/LCF/Makefile
--- a/src/LCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -28,13 +28,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LCF;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -17,6 +17,4 @@
 use"pair.ML";
 use"fix.ML";
 
-make_chart ();   (*make HTML chart*)
-
 val LCF_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/LK/Makefile
--- a/src/LK/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LK/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,13 +29,13 @@
 	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LK;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK;\
+		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/LK/ROOT.ML
--- a/src/LK/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LK/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -19,6 +19,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val LK_build_completed = ();	(*indicate successful build*)
diff -r 6bdee79ef125 -r 90d615b599d9 src/Modal/Makefile
--- a/src/Modal/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Modal/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,14 +29,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Modal;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
                        | $(BIN)/LK;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/Modal/ROOT.ML
--- a/src/Modal/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Modal/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -78,8 +78,6 @@
 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 6bdee79ef125 -r 90d615b599d9 src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/ZF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -38,13 +38,13 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/ZF;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\
+		else echo 'open PolyML; exit_use_dir".";' | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
diff -r 6bdee79ef125 -r 90d615b599d9 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/ZF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 (*printing functions are inherited from FOL*)
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val ZF_build_completed = ();	(*indicate successful build*)