#########################################################################
#									#
# 			Makefile for Elle (ELAB)			#
#									#
#########################################################################

#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 elab_obj.thy  elab_obj.ML \
         elab_atexp.thy elab_exprow.thy elab_exp.thy elab_match.thy \
         elab_mrule.thy elab_dec.thy elab_valbind.thy elab_typbind.thy \
         elab_datbind.thy elab_conbind.thy elab_exbind.thy elab_atpat.thy \
         elab_patrow.thy elab_pat.thy elab_ty.thy \
         elab_tyrow.thy elab_tyseq.thy elab_program.thy  ElabProver.ML

TESTFILES = Test1.ML Test2.ML Test3.ML Test4.ML Test5.ML Test6.ML

$(LOCALBIN)/ELAB:   $(LOCALBIN)/KERNEL  $(FILES) 
	case "$(COMP)" in \
	poly*)	echo 'make_database"$(LOCALBIN)/ELAB"; quit();'  \
			| $(COMP) $(LOCALBIN)/KERNEL;\
		echo 'open PolyML; use"ROOT";' | $(COMP) $(LOCALBIN)/ELAB;;\
	sml*)	echo 'use"ROOT.ML"; xML"$(LOCALBIN)/ELAB" banner;' \
                          | $(LOCALBIN)/KERNEL;;\
	*)	echo Bad value for ISABELLECOMP;;\
	esac

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

.PRECIOUS:   $(LOCALBIN)/KERNEL  $(LOCALBIN)/ELAB 
