# HG changeset patch
# User clasohm
# Date 823975461 -3600
# Node ID 38a14548baadd073a83f606fe13a5f40420f6bd4
# Parent  713256365b927ddec3e37a33769fb74238c4fcc7
make_html now only remains set if MAKE_HTML=true

diff -r 713256365b92 -r 38a14548baad src/CCL/Makefile
--- a/src/CCL/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/CCL/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -36,14 +36,19 @@
 $(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)  $(CCL_FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CCL;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CCL;\
+                else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CCL;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)   if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CCL" banner;' \
+                       | $(BIN)/FOL;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
@@ -56,9 +61,16 @@
 
 test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' \
-                  | $(COMP) $(BIN)/CCL ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CCL;;\
+	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
+                       | $(COMP) $(BIN)/CCL;\
+                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CCL;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex";' \
+                       | $(BIN)/CCL;\
+                else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 713256365b92 -r 38a14548baad src/CTT/Makefile
--- a/src/CTT/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/CTT/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -35,14 +35,19 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CTT;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CTT;\
+                else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CTT;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CTT" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
diff -r 713256365b92 -r 38a14548baad src/Cube/Makefile
--- a/src/Cube/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/Cube/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -28,14 +28,19 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Cube;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Cube;\
+                else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Cube;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Cube" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
diff -r 713256365b92 -r 38a14548baad src/FOL/Makefile
--- a/src/FOL/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/FOL/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -39,14 +39,19 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
 		  | $(COMP) $(BIN)/Pure;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOL;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOL;\
+                else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOL;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOL" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
@@ -59,8 +64,16 @@
 
 test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOL;;\
+	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
+                       | $(COMP) $(BIN)/FOL;\
+                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex";' \
+                       | $(BIN)/FOL;\
+                else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 713256365b92 -r 38a14548baad src/FOLP/Makefile
--- a/src/FOLP/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/FOLP/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -32,14 +32,19 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOLP;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOLP;\
+                else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/FOLP;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOLP" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
@@ -52,8 +57,16 @@
 
 test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOLP;;\
+	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
+                       | $(COMP) $(BIN)/FOLP;\
+                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex";' \
+                       | $(BIN)/FOLP;\
+                else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 713256365b92 -r 38a14548baad src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/HOL/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -40,14 +40,19 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-                  | $(COMP) $(BIN)/HOL;\
-		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/HOL;\
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
+                else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOL;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOL" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
@@ -73,14 +78,21 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:    $(BIN)/HOL  $(IMP_FILES)
-	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
+        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
+        fi
 
 ##Hoare logic
 Hoare_NAMES = Hoare Arith2 Examples
-Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
+Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
+              $(Hoare_NAMES:%=Hoare/%.ML)
 
 Hoare:  $(BIN)/HOL  $(Hoare_FILES)
-	echo 'exit_use_dir"Hoare";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
+        fi
 
 ##The integers in HOL
 INTEG_NAMES = Equiv Integ 
@@ -89,7 +101,10 @@
               $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
 Integ:  $(BIN)/HOL  $(INTEG_FILES)
-	echo 'exit_use_dir"Integ";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
+        fi
 
 ##I/O Automata
 IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
@@ -106,8 +121,14 @@
  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
 
 IOA:    $(BIN)/HOL  $(IOA_FILES)
-	echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC)
-	echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
+               | $(LOGIC);\
+             echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
+               | $(LOGIC);\
+        else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
+	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
+        fi
 
 ##Properties of substitutions
 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
@@ -116,7 +137,10 @@
               $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
 Subst:  $(BIN)/HOL  $(SUBST_FILES)
-	echo 'exit_use_dir"Subst";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
+        fi
 
 ##Confluence of Lambda-calculus
 LAMBDA_NAMES = Lambda ParRed Commutation Eta
@@ -125,7 +149,11 @@
               $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
 Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
-	echo 'exit_use_dir"Lambda";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
+               | $(LOGIC);\
+        else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
+        fi
 
 ##Type inference for MiniML
 MINIML_NAMES = I Maybe MiniML Type W
@@ -134,7 +162,11 @@
               $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
 MiniML: $(BIN)/HOL  $(MINIML_FILES)
-	echo 'exit_use_dir"MiniML";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
+               | $(LOGIC);\
+        else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
+        fi
 
 ##Lexical analysis
 LEX_FILES = Auto AutoChopper Chopper Prefix
@@ -143,7 +175,10 @@
             $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
 Lex:	$(BIN)/HOL  $(LEX_FILES)
-	echo 'exit_use_dir"Lex";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
+        fi
 
 ##Miscellaneous examples
 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
@@ -153,7 +188,10 @@
            ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:     $(BIN)/HOL  $(EX_FILES)
-	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
+        fi
 
 #Full test.
 test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
diff -r 713256365b92 -r 38a14548baad src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/HOLCF/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -36,14 +36,19 @@
 $(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOLCF;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOLCF;\
+                else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/HOLCF;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOLCF" banner;' \
+                       | $(BIN)/HOL;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
                        | $(BIN)/HOL;\
                 fi;;\
@@ -61,8 +66,16 @@
 
 test:   ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
-	sml*)	echo 'exit_use_dir"ex"' | $(BIN)/HOLCF;;\
+	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
+                       | $(COMP) $(BIN)/HOLCF;\
+                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"ex";' \
+                       | $(BIN)/HOLCF;\
+                else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
@@ -77,9 +90,16 @@
 
 test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use_dir"explicit_domains"; quit();' \
-                  | $(COMP) $(BIN)/HOLCF ;;\
-	sml*)	echo 'exit_use_dir"explicit_domains"' | $(BIN)/HOLCF;;\
+	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"explicit_domains";                             quit();' | $(COMP) $(BIN)/HOLCF;\
+                else echo 'exit_use_dir"explicit_domains"; quit();' \
+                       | $(COMP) $(BIN)/HOLCF;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
+                       | $(BIN)/HOLCF;\
+                else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r 713256365b92 -r 38a14548baad src/LCF/Makefile
--- a/src/LCF/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/LCF/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -27,14 +27,19 @@
 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LCF;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LCF;\
+                else echo 'open PolyML; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LCF;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/LCF" banner;' \
+                       | $(BIN)/FOL;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
diff -r 713256365b92 -r 38a14548baad src/LK/Makefile
--- a/src/LK/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/LK/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -28,13 +28,18 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LK;\
-		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LK;\
+                else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/LK" banner;' \
+                       | $(BIN)/Pure;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
diff -r 713256365b92 -r 38a14548baad src/Modal/Makefile
--- a/src/Modal/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/Modal/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -28,14 +28,19 @@
 $(BIN)/Modal:   $(BIN)/LK  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Modal;\
-		else echo 'open PolyML; exit_use_dir".";' \
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Modal;\
+                else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Modal;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Modal" banner;' \
+                       | $(BIN)/LK;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
                        | $(BIN)/LK;\
                 fi;;\
diff -r 713256365b92 -r 38a14548baad src/ZF/Makefile
--- a/src/ZF/Makefile	Fri Feb 09 18:56:39 1996 +0100
+++ b/src/ZF/Makefile	Sat Feb 10 19:04:21 1996 +0100
@@ -37,13 +37,19 @@
 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
-                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/ZF;\
-		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/ZF;\
+		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
+                else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/ZF;\
                 fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
+                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/ZF" banner;' \
+                       | $(BIN)/FOL;\
                 else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
@@ -69,7 +75,10 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:   $(BIN)/ZF  $(IMP_FILES)
-	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
+        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
+        fi
 
 ##Coinduction example
 COIND_NAMES = ECR Language MT Map Static Types Values 
@@ -78,7 +87,10 @@
               $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
 
 Coind:  $(BIN)/ZF  $(COIND_FILES)
-	echo 'exit_use_dir"Coind";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
+        fi
 
 ##AC examples
 AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
@@ -92,7 +104,10 @@
            $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
 
 AC:  $(BIN)/ZF  $(AC_FILES)
-	echo 'exit_use_dir"AC";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
+        else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
+        fi
 
 ##Residuals example
 
@@ -103,7 +118,10 @@
                             $(RESID_NAMES:%=Resid/%.ML)
 
 Resid:  $(BIN)/ZF  $(RESID_FILES)
-	echo 'exit_use_dir"Resid";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
+        else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
+        fi
 
 ##Miscellaneous examples
 EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
@@ -113,7 +131,10 @@
 
 #Test ZF by loading the examples in directory ex
 ex:     $(BIN)/ZF  $(EX_FILES)
-	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
+	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
+        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
+        fi
 
 #Full test.
 test:   $(BIN)/ZF IMP Coind AC Resid ex