equal
deleted
inserted
replaced
28 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle |
28 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle |
29 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML\ |
29 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML\ |
30 ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
30 ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
31 |
31 |
32 $(BIN)/FOL: $(BIN)/Pure $(FILES) |
32 $(BIN)/FOL: $(BIN)/Pure $(FILES) |
33 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
33 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
34 then echo Bad value for ISABELLEBIN: \ |
34 then echo Bad value for ISABELLEBIN: \ |
35 $(BIN) is the Isabelle source directory; \ |
35 $(BIN) is the Isabelle source directory; \ |
36 exit 1; \ |
36 exit 1; \ |
37 fi;\ |
37 fi |
38 case "$(COMP)" in \ |
38 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
39 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
39 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
40 | $(COMP) $(BIN)/Pure;\ |
40 | $(COMP) $(BIN)/Pure;\ |
41 if [ "$${MAKE_HTML}" = "true" ]; \ |
41 if [ "$${MAKE_HTML}" = "true" ]; \ |
42 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
42 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
43 | $(COMP) $(BIN)/FOL;\ |
43 | $(COMP) $(BIN)/FOL;\ |
54 | $(BIN)/Pure;\ |
54 | $(BIN)/Pure;\ |
55 else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \ |
55 else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \ |
56 | $(BIN)/Pure;\ |
56 | $(BIN)/Pure;\ |
57 fi;;\ |
57 fi;;\ |
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 $(BIN)/Pure: |
62 $(BIN)/Pure: |
63 cd ../Pure; $(MAKE) |
63 cd ../Pure; $(MAKE) |
64 |
64 |
65 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
65 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
66 case "$(COMP)" in \ |
66 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
67 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
67 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
68 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
68 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
69 | $(COMP) $(BIN)/FOL;\ |
69 | $(COMP) $(BIN)/FOL;\ |
70 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\ |
70 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\ |
71 fi;;\ |
71 fi;;\ |
73 then echo 'make_html := true; exit_use_dir"ex";' \ |
73 then echo 'make_html := true; exit_use_dir"ex";' \ |
74 | $(BIN)/FOL;\ |
74 | $(BIN)/FOL;\ |
75 else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\ |
75 else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\ |
76 fi;;\ |
76 fi;;\ |
77 *) echo Bad value for ISABELLECOMP: \ |
77 *) echo Bad value for ISABELLECOMP: \ |
78 $(COMP) is not poly or sml;;\ |
78 \"$(COMP)\" is not poly or sml;;\ |
79 esac |
79 esac |
80 |
80 |
81 .PRECIOUS: $(BIN)/Pure $(BIN)/FOL |
81 .PRECIOUS: $(BIN)/Pure $(BIN)/FOL |