src/FOLP/Makefile
changeset 2117 292df12bace5
parent 2094 2061df98aab5
child 2235 866dbb04816c
equal deleted inserted replaced
2116:73bbf2cc7651 2117:292df12bace5
    27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\
    27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\
    28 	   ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\
    28 	   ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\
    29 	   ex/prop.ML ex/quant.ML
    29 	   ex/prop.ML ex/quant.ML
    30 
    30 
    31 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
    31 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
    32 	case "$(COMP)" in \
    32 	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    33 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    33 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    34 			| $(COMP) $(BIN)/Pure;\
    34 			| $(COMP) $(BIN)/Pure;\
    35 		if [ "$${MAKE_HTML}" = "true" ]; \
    35 		if [ "$${MAKE_HTML}" = "true" ]; \
    36 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    36 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    37 		       | $(COMP) $(BIN)/FOLP;\
    37 		       | $(COMP) $(BIN)/FOLP;\
    48 		       | $(BIN)/Pure;\
    48 		       | $(BIN)/Pure;\
    49 		else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    49 		else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    50 		       | $(BIN)/Pure;\
    50 		       | $(BIN)/Pure;\
    51 		fi;;\
    51 		fi;;\
    52 	*)	echo Bad value for ISABELLECOMP: \
    52 	*)	echo Bad value for ISABELLECOMP: \
    53 			$(COMP) is not poly or sml;;\
    53 			\"$(COMP)\" is not poly or sml;;\
    54 	esac
    54 	esac
    55 
    55 
    56 $(BIN)/Pure:
    56 $(BIN)/Pure:
    57 	cd ../Pure;  $(MAKE)
    57 	cd ../Pure;  $(MAKE)
    58 
    58 
    59 test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
    59 test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
    60 	case "$(COMP)" in \
    60 	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    61 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    61 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    62 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    62 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    63 		       | $(COMP) $(BIN)/FOLP;\
    63 		       | $(COMP) $(BIN)/FOLP;\
    64 		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
    64 		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
    65 		fi;;\
    65 		fi;;\
    67 		then echo 'make_html := true; exit_use_dir"ex";' \
    67 		then echo 'make_html := true; exit_use_dir"ex";' \
    68 		       | $(BIN)/FOLP;\
    68 		       | $(BIN)/FOLP;\
    69 		else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
    69 		else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
    70 		fi;;\
    70 		fi;;\
    71 	*)	echo Bad value for ISABELLECOMP: \
    71 	*)	echo Bad value for ISABELLECOMP: \
    72 			$(COMP) is not poly or sml;;\
    72 			\"$(COMP)\" is not poly or sml;;\
    73 	esac
    73 	esac
    74 
    74 
    75 .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOLP 
    75 .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOLP