#########################################################################
#									#
# 			Makefile for Elle (Kernel)			#
#									#
#########################################################################

#To make the system, cd to this directory and type
#	make -f Makefile 

#Environment variable ISABELLECOMP specifies the compiler.
#Environment variable ISABELLEBIN specifies the directory containing 
#                     the images for Isabelle object logics.
#Environment variable ISABELLELOCALBIN specifies the destination directory for 
#                     Elle images.
#For Poly/ML, ISABELLEBIN and ISABELLE must begin with a /


BIN = $(ISABELLEBIN)
LOCALBIN = $(ISABELLELOCALBIN)
COMP = $(ISABELLECOMP)
FILES = ROOT.ML Tools.ML More_ZF.ML More_Arith.ML map.thy map.ML overwrite.thy\
        overwrite.ML zf_ext.thy zf_ext.ML tags.thy tags.ML \
        identifiers.thy identifiers.ML sml_syntax.thy kernel.thy kernel.ML

TESTFILES = Test.ML

#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(LOCALBIN)/KERNEL:   $(BIN)/ZF  $(FILES) 
	case "$(COMP)" in \
	poly*)	cp $(BIN)/ZF $(LOCALBIN)/KERNEL;\
		echo 'use"ROOT";' | $(COMP) $(LOCALBIN)/KERNEL ;;\
	sml*)	echo 'use"ROOT.ML"; xML"$(LOCALBIN)/KERNEL" banner;' \
                | $(BIN)/ZF;;\
	*)	echo Bad value for ISABELLECOMP;;\
	esac


test:	$(TESTFILES)
	case "$(COMP)" in \
	poly*)  echo 'use "Test"' \
                     | $(COMP) $(LOCALBIN)/KERNEL;;\
	sml*)	echo 'use "Test.ML"' \
                     | $(LOCALBIN)/KERNEL;;\
	*)	echo Bad value for ISABELLECOMP;;\
	esac

.PRECIOUS:  $(BIN)/ZF $(LOCALBIN)/KERNEL 
