src/Pure/Makefile
changeset 2094 2061df98aab5
parent 2023 aa25f20c5d8b
child 2117 292df12bace5
     1.1 --- a/src/Pure/Makefile	Mon Oct 14 11:08:54 1996 +0200
     1.2 +++ b/src/Pure/Makefile	Tue Oct 15 10:46:42 1996 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  #  $Id$
     1.5  #########################################################################
     1.6  #									#
     1.7 -# 			Makefile for Isabelle (Pure)			#
     1.8 +#			Makefile for Isabelle (Pure)			#
     1.9  #									#
    1.10  #########################################################################
    1.11  
    1.12 @@ -24,10 +24,10 @@
    1.13  FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
    1.14  	sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
    1.15  	net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
    1.16 -        goals.ML axclass.ML install_pp.ML\
    1.17 -        NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
    1.18 +	goals.ML axclass.ML install_pp.ML\
    1.19 +	NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
    1.20  
    1.21 -SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
    1.22 +SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
    1.23  	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
    1.24  	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
    1.25  	Syntax/syn_ext.ML	Syntax/mixfix.ML
    1.26 @@ -36,25 +36,24 @@
    1.27  	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML
    1.28  
    1.29  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.30 -$(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)
    1.31 +$(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
    1.32  	case "$(COMP)" in \
    1.33  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    1.34  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    1.35  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
    1.36 -                  | $(COMP) $(BIN)/Pure;\
    1.37 +		  | $(COMP) $(BIN)/Pure;\
    1.38  		discgarb -c $(BIN)/Pure;;\
    1.39  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
    1.40 -           	then echo Bad value for ISABELLEBIN: \
    1.41 -                	$(BIN) is not a writable directory; \
    1.42 -                	exit 1; \
    1.43 -           	fi;\
    1.44 -		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;                                    xML"$(BIN)/Pure" banner;' | $(COMP);;\
    1.45 +		then echo Bad value for ISABELLEBIN: \
    1.46 +			$(BIN) is not a writable directory; \
    1.47 +			exit 1; \
    1.48 +		fi;\
    1.49 +		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
    1.50  	*)	echo Bad value for ISABELLECOMP: \
    1.51 -                	$(COMP) is not poly or sml;;\
    1.52 +			$(COMP) is not poly or sml;;\
    1.53  	esac
    1.54  
    1.55  
    1.56  test: $(BIN)/Pure
    1.57 -	
    1.58  
    1.59 -.PRECIOUS:  $(BIN)/Pure  
    1.60 +.PRECIOUS:  $(BIN)/Pure