#########################################################################
#									#
# 			Makefile for ELLE (combined system)		#
#									#
#########################################################################

#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)
EVAL = ../Eval
ELAB = ../Elab

FILES =  $(EVAL)/ROOT.ML $(EVAL)/EvalProver.ML \
         $(EVAL)/eval_obj.thy $(EVAL)/eval_obj.ML \
         $(EVAL)/eval_atexp.thy $(EVAL)/eval_exprow.thy $(EVAL)/eval_exp.thy \
         $(EVAL)/eval_match.thy $(EVAL)/eval_mrule.thy $(EVAL)/eval_dec.thy \
         $(EVAL)/eval_valbind.thy $(EVAL)/eval_atpat.thy \
         $(EVAL)/eval_patrow.thy $(EVAL)/eval_pat.thy $(EVAL)/eval_program.thy \
         ROOT.ML  Elle.ML

TESTFILES =  Test.ML

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

	

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

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