src/ZF/Makefile
changeset 1491 38a14548baad
parent 1361 90d615b599d9
child 1607 5c123831c4e2
--- 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