src/Cube/IsaMakefile
changeset 2819 ebeacfa0e56b
parent 2487 4f0bf2936bc0
child 3118 24dae6222579
equal deleted inserted replaced
2818:b47926f28b21 2819:ebeacfa0e56b
     6 
     6 
     7 OUT = $(ISABELLE_OUTPUT_DIR)
     7 OUT = $(ISABELLE_OUTPUT_DIR)
     8 FILES =	ROOT.ML Cube.thy Cube.ML
     8 FILES =	ROOT.ML Cube.thy Cube.ML
     9 
     9 
    10 $(OUT)/Cube: $(OUT)/Pure $(FILES)
    10 $(OUT)/Cube: $(OUT)/Pure $(FILES)
    11 	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure Cube
    11 	@$(ISATOOL) usedir -b $(OUT)/Pure Cube
    12 	@chmod -w $@
    12 	@chmod -w $@
    13 
    13 
    14 $(OUT)/Pure:
    14 $(OUT)/Pure:
    15 	@cd ../Pure; $(ISATOOL) make
    15 	@cd ../Pure; $(ISATOOL) make
    16 
    16 
    17 test: ex.ML $(OUT)/Cube
    17 test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube
    18 	@$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); use"ex.ML"; quit();' \
    18 	@$(ISATOOL) usedir $(OUT)/Cube ex
    19 	  -rq $(OUT)/Cube
       
    20 
    19 
    21 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube
    20 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube