--- a/src/CCL/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/CCL/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -34,7 +34,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) cp $(BIN)/FOL $(BIN)/CCL;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -54,14 +54,14 @@
| $(BIN)/FOL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/FOL:
cd ../FOL; $(MAKE)
test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"ex"; quit();' \
| $(COMP) $(BIN)/CCL;\
@@ -73,7 +73,7 @@
else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/FOL $(BIN)/CCL
--- a/src/CTT/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/CTT/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -27,12 +27,12 @@
EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
$(BIN)/CTT: $(BIN)/Pure $(FILES)
- if [ -d $${ISABELLEBIN:?}/Pure ];\
+ @if [ -d $${ISABELLEBIN:?}/Pure ];\
then echo Bad value for ISABELLEBIN: \
$(BIN) is the Isabelle source directory; \
exit 1; \
- fi;\
- case "$(COMP)" in \
+ fi
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/CTT"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -53,18 +53,18 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/CTT
--- a/src/Cube/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Cube/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -25,7 +25,7 @@
FILES = ROOT.ML Cube.thy Cube.ML
$(BIN)/Cube: $(BIN)/Pure $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/Cube"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -46,18 +46,18 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
test: ex.ML $(BIN)/Cube
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
sml*) echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/Cube
--- a/src/FOL/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/FOL/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -30,12 +30,12 @@
ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
$(BIN)/FOL: $(BIN)/Pure $(FILES)
- if [ -d $${ISABELLEBIN:?}/Pure ];\
+ @if [ -d $${ISABELLEBIN:?}/Pure ];\
then echo Bad value for ISABELLEBIN: \
$(BIN) is the Isabelle source directory; \
exit 1; \
- fi;\
- case "$(COMP)" in \
+ fi
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/FOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -56,14 +56,14 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"ex"; quit();' \
| $(COMP) $(BIN)/FOL;\
@@ -75,7 +75,7 @@
else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/FOL
--- a/src/FOLP/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/FOLP/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -29,7 +29,7 @@
ex/prop.ML ex/quant.ML
$(BIN)/FOLP: $(BIN)/Pure $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -50,14 +50,14 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"ex"; quit();' \
| $(COMP) $(BIN)/FOLP;\
@@ -69,7 +69,7 @@
else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/FOLP
--- a/src/HOL/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/HOL/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -33,12 +33,12 @@
$(NAMES:%=%.thy) $(NAMES:%=%.ML)
$(BIN)/HOL: $(BIN)/Pure $(FILES)
- if [ -d $${ISABELLEBIN:?}/Pure ];\
+ @if [ -d $${ISABELLEBIN:?}/Pure ];\
then echo Bad value for ISABELLEBIN: \
$(BIN) is the Isabelle source directory; \
exit 1; \
- fi;\
- case "$(COMP)" in \
+ fi
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/HOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -59,7 +59,7 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml; exit 1;;\
+ \"$(COMP)\" is not poly or sml; exit 1;;\
esac
$(BIN)/Pure:
@@ -68,11 +68,11 @@
#### Testing of HOL
#A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
+LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
sml*) echo "$ISABELLEBIN/HOL" ;;\
- *) echo "echo Bad value for ISABELLECOMP: \
- $ISABELLEBIN is not poly or sml; exit 1" ;;\
+ *) echo "echo; echo Bad value for ISABELLECOMP: \
+ $ISABELLECOMP is not poly or sml; exit 1" ;;\
esac
##IMP-semantics example
@@ -80,7 +80,7 @@
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
IMP: $(BIN)/HOL $(IMP_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -91,7 +91,7 @@
$(Hoare_NAMES:%=Hoare/%.ML)
Hoare: $(BIN)/HOL $(Hoare_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -103,7 +103,7 @@
$(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
Integ: $(BIN)/HOL $(INTEG_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -123,7 +123,7 @@
$(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
IOA: $(BIN)/HOL $(IOA_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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();' \
@@ -134,12 +134,13 @@
##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
+Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
+ Yahalom Yahalom2
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
Auth: $(BIN)/HOL $(AUTH_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
fi
@@ -152,7 +153,7 @@
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
Subst: $(BIN)/HOL $(SUBST_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -164,7 +165,7 @@
$(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
Lambda: $(BIN)/HOL $(LAMBDA_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
| $(LOGIC);\
else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
@@ -177,7 +178,7 @@
$(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
MiniML: $(BIN)/HOL $(MINIML_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
| $(LOGIC);\
else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
@@ -190,7 +191,7 @@
$(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
Lex: $(BIN)/HOL $(LEX_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -203,7 +204,7 @@
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
ex: $(BIN)/HOL $(EX_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
--- a/src/HOLCF/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/HOLCF/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -34,7 +34,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -54,7 +54,7 @@
| $(BIN)/HOL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/HOL:
@@ -66,7 +66,7 @@
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
then echo 'make_html := true; exit_use_dir"ex"; quit();' \
| $(COMP) $(BIN)/HOLCF;\
@@ -78,7 +78,7 @@
else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
@@ -90,7 +90,7 @@
$(EXPLICIT_DOMAINS_THYS:.thy=.ML)
test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
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();' \
@@ -102,7 +102,7 @@
else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
--- a/src/LCF/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/LCF/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -25,7 +25,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/LCF: $(BIN)/FOL $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) cp $(BIN)/FOL $(BIN)/LCF;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -45,18 +45,18 @@
| $(BIN)/FOL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
(BIN)/FOL:
cd ../FOL; $(MAKE)
test: ex.ML $(BIN)/LCF
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
sml*) echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/FOL $(BIN)/LCF
--- a/src/Pure/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Pure/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -37,7 +37,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
@@ -50,7 +50,7 @@
fi;\
echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
--- a/src/Sequents/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/Sequents/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -32,7 +32,7 @@
$(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
$(BIN)/Sequents: $(BIN)/Pure $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \
| $(COMP) $(BIN)/Pure;\
if [ "$${MAKE_HTML}" = "true" ]; \
@@ -52,18 +52,18 @@
| $(BIN)/Pure;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
test: $(BIN)/Sequents $(EX_FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ \"$(COMP)\" is not poly or sml;;\
esac
--- a/src/ZF/Makefile Mon Oct 21 09:51:18 1996 +0200
+++ b/src/ZF/Makefile Mon Oct 21 11:18:34 1996 +0200
@@ -35,7 +35,7 @@
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/ZF: $(BIN)/FOL $(FILES)
- case "$(COMP)" in \
+ @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
poly*) cp $(BIN)/FOL $(BIN)/ZF;\
if [ "$${MAKE_HTML}" = "true" ]; \
then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -55,7 +55,7 @@
| $(BIN)/FOL;\
fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml; exit 1;;\
+ \"$(COMP)\" is not poly or sml; exit 1;;\
esac
$(BIN)/FOL:
@@ -64,11 +64,11 @@
#### Testing of ZF
#A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
+LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
poly*) echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
sml*) echo "$ISABELLEBIN/ZF" ;;\
- *) echo "echo Bad value for ISABELLECOMP: \
- $ISABELLEBIN is not poly or sml; exit 1" ;;\
+ *) echo "echo; echo Bad value for ISABELLECOMP: \
+ $ISABELLECOMP is not poly or sml; exit 1" ;;\
esac
##IMP-semantics example
@@ -76,7 +76,7 @@
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
IMP: $(BIN)/ZF $(IMP_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -88,7 +88,7 @@
$(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
Coind: $(BIN)/ZF $(COIND_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -105,7 +105,7 @@
$(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
AC: $(BIN)/ZF $(AC_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -119,7 +119,7 @@
$(RESID_NAMES:%=Resid/%.ML)
Resid: $(BIN)/ZF $(RESID_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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
@@ -132,7 +132,7 @@
#Test ZF by loading the examples in directory ex
ex: $(BIN)/ZF $(EX_FILES)
- if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ @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