src/LCF/Makefile
changeset 2117 292df12bace5
parent 2094 2061df98aab5
child 2235 866dbb04816c
equal deleted inserted replaced
2116:73bbf2cc7651 2117:292df12bace5
    23 COMP = $(ISABELLECOMP)
    23 COMP = $(ISABELLECOMP)
    24 FILES =	 ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    24 FILES =	 ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    25 
    25 
    26 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    26 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    27 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
    27 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
    28 	case "$(COMP)" in \
    28 	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    29 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
    29 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
    30 		if [ "$${MAKE_HTML}" = "true" ]; \
    30 		if [ "$${MAKE_HTML}" = "true" ]; \
    31 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    31 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    32 		       | $(COMP) $(BIN)/LCF;\
    32 		       | $(COMP) $(BIN)/LCF;\
    33 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    33 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    43 		       | $(BIN)/FOL;\
    43 		       | $(BIN)/FOL;\
    44 		else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
    44 		else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
    45 		       | $(BIN)/FOL;\
    45 		       | $(BIN)/FOL;\
    46 		fi;;\
    46 		fi;;\
    47 	*)	echo Bad value for ISABELLECOMP: \
    47 	*)	echo Bad value for ISABELLECOMP: \
    48 			$(COMP) is not poly or sml;;\
    48 			\"$(COMP)\" is not poly or sml;;\
    49 	esac
    49 	esac
    50 
    50 
    51 (BIN)/FOL:
    51 (BIN)/FOL:
    52 	cd ../FOL;  $(MAKE)
    52 	cd ../FOL;  $(MAKE)
    53 
    53 
    54 test:	ex.ML  $(BIN)/LCF
    54 test:	ex.ML  $(BIN)/LCF
    55 	case "$(COMP)" in \
    55 	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    56 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
    56 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
    57 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
    57 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
    58 	*)	echo Bad value for ISABELLECOMP: \
    58 	*)	echo Bad value for ISABELLECOMP: \
    59 			$(COMP) is not poly or sml;;\
    59 			\"$(COMP)\" is not poly or sml;;\
    60 	esac
    60 	esac
    61 
    61 
    62 .PRECIOUS:   $(BIN)/FOL	 $(BIN)/LCF 
    62 .PRECIOUS:   $(BIN)/FOL	 $(BIN)/LCF