equal
deleted
inserted
replaced
25 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
25 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
26 |
26 |
27 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
27 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
28 |
28 |
29 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
29 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
30 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
30 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
31 then echo Bad value for ISABELLEBIN: \ |
31 then echo Bad value for ISABELLEBIN: \ |
32 $(BIN) is the Isabelle source directory; \ |
32 $(BIN) is the Isabelle source directory; \ |
33 exit 1; \ |
33 exit 1; \ |
34 fi;\ |
34 fi |
35 case "$(COMP)" in \ |
35 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
36 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
36 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
37 | $(COMP) $(BIN)/Pure;\ |
37 | $(COMP) $(BIN)/Pure;\ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
40 | $(COMP) $(BIN)/CTT;\ |
40 | $(COMP) $(BIN)/CTT;\ |
51 | $(BIN)/Pure;\ |
51 | $(BIN)/Pure;\ |
52 else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \ |
52 else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \ |
53 | $(BIN)/Pure;\ |
53 | $(BIN)/Pure;\ |
54 fi;;\ |
54 fi;;\ |
55 *) echo Bad value for ISABELLECOMP: \ |
55 *) echo Bad value for ISABELLECOMP: \ |
56 $(COMP) is not poly or sml;;\ |
56 \"$(COMP)\" is not poly or sml;;\ |
57 esac |
57 esac |
58 |
58 |
59 $(BIN)/Pure: |
59 $(BIN)/Pure: |
60 cd ../Pure; $(MAKE) |
60 cd ../Pure; $(MAKE) |
61 |
61 |
62 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
62 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
63 case "$(COMP)" in \ |
63 @case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
64 poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
64 poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
65 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
65 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
66 *) echo Bad value for ISABELLECOMP: \ |
66 *) echo Bad value for ISABELLECOMP: \ |
67 $(COMP) is not poly or sml;;\ |
67 \"$(COMP)\" is not poly or sml;;\ |
68 esac |
68 esac |
69 |
69 |
70 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |
70 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |