equal
deleted
inserted
replaced
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 |