# HG changeset patch
# User paulson
# Date 849087065 -3600
# Node ID 866dbb04816c8ca6ea25cf35eb5e35c23d66ad39
# Parent  041bf27011b1d95d43f2dc6fb47d86b06cd63ef7
Makefile improvements by Thomas Santen and Stephan Herrmann
Should be more portable across different versions of make

diff -r 041bf27011b1 -r 866dbb04816c src/CCL/Makefile
--- a/src/CCL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/CCL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -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 `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -61,7 +61,7 @@
 	cd ../FOL;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/CCL	$(EX_FILES)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/CCL;\
diff -r 041bf27011b1 -r 866dbb04816c src/CTT/Makefile
--- a/src/CTT/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/CTT/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -32,7 +32,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -60,7 +60,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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: \
diff -r 041bf27011b1 -r 866dbb04816c src/Cube/Makefile
--- a/src/Cube/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Cube/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -25,7 +25,7 @@
 FILES =		ROOT.ML	 Cube.thy  Cube.ML
 
 $(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -53,7 +53,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex.ML $(BIN)/Cube
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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: \
diff -r 041bf27011b1 -r 866dbb04816c src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/FOL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -35,7 +35,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -63,7 +63,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOL;\
diff -r 041bf27011b1 -r 866dbb04816c src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/FOLP/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -29,7 +29,7 @@
 	   ex/prop.ML ex/quant.ML
 
 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -57,7 +57,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOLP;\
diff -r 041bf27011b1 -r 866dbb04816c src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/HOL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -38,7 +38,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -68,12 +68,13 @@
 #### Testing of HOL
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
-	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
-	sml*)	echo "$ISABELLEBIN/HOL" ;;\
+#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
+LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
+	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
+	sml*)	echo "$(ISABELLEBIN)/HOL" ;;\
 	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$ISABELLECOMP is not poly or sml; exit 1" ;;\
-	esac
+			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
+	esac`
 
 ##IMP-semantics example
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
@@ -197,8 +198,8 @@
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
-	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd Group Ring Lagrange \
+	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
diff -r 041bf27011b1 -r 866dbb04816c src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/HOLCF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -34,7 +34,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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".";' \
@@ -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 `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/HOLCF;\
@@ -90,7 +90,7 @@
 			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
 
 test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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();' \
diff -r 041bf27011b1 -r 866dbb04816c src/LCF/Makefile
--- a/src/LCF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/LCF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -25,7 +25,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -52,7 +52,7 @@
 	cd ../FOL;  $(MAKE)
 
 test:	ex.ML  $(BIN)/LCF
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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: \
diff -r 041bf27011b1 -r 866dbb04816c src/Pure/Makefile
--- a/src/Pure/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Pure/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -21,7 +21,8 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
+FILES =	POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\
+	term.ML symtab.ML type.ML sign.ML\
 	sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
 	net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
 	goals.ML axclass.ML install_pp.ML\
@@ -37,7 +38,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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;' \
@@ -49,8 +50,8 @@
 			exit 1; \
 		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;;\
+	*)	echo Bad value for ISABELLECOMP: $(COMP); \
+		echo "   " \"`basename "$(COMP)"`\" is not poly or sml;;\
 	esac
 
 
diff -r 041bf27011b1 -r 866dbb04816c src/Sequents/Makefile
--- a/src/Sequents/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Sequents/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -32,7 +32,7 @@
     $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
 
 $(BIN)/Sequents:   $(BIN)/Pure	$(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'	\
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -59,7 +59,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	$(BIN)/Sequents	 $(EX_FILES)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(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: \
diff -r 041bf27011b1 -r 866dbb04816c src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/ZF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -35,7 +35,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/ZF:   $(BIN)/FOL	 $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -64,12 +64,13 @@
 #### Testing of ZF
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
-	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
-	sml*)	echo "$ISABELLEBIN/ZF" ;;\
+#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
+LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
+	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/ZF" ;;\
+	sml*)	echo "$(ISABELLEBIN)/ZF" ;;\
 	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$ISABELLECOMP is not poly or sml; exit 1" ;;\
-	esac
+			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
+	esac`
 
 ##IMP-semantics example
 IMP_NAMES = Com Denotation Equiv