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