--- 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
--- 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;;\
--- 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;;\
--- 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
--- 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
--- 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
--- 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
--- 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;;\
--- 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;;\
--- 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;;\
--- 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