src/HOL/Makefile
changeset 1296 ae31bb7774a7
parent 1270 e3a391e848a9
child 1301 42782316d510
     1.1 --- a/src/HOL/Makefile	Tue Oct 24 14:49:45 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Tue Oct 24 14:50:24 1995 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +# $Id$
     1.5  #########################################################################
     1.6  #									#
     1.7  # 			Makefile for Isabelle (HOL)			#
     1.8 @@ -5,9 +6,11 @@
     1.9  #########################################################################
    1.10  
    1.11  #To make the system, cd to this directory and type  
    1.12 -#	make -f Makefile 
    1.13 +#	make
    1.14  #To make the system and test it on standard examples, type  
    1.15 -#	make -f Makefile test
    1.16 +#	make test
    1.17 +#To generate HTML files for every theory, set the environment variable
    1.18 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    1.19  
    1.20  #Environment variable ISABELLECOMP specifies the compiler.
    1.21  #Environment variable ISABELLEBIN specifies the destination directory.
    1.22 @@ -36,9 +39,17 @@
    1.23             	fi;\
    1.24  	case "$(COMP)" in \
    1.25  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
    1.26 -			| $(COMP) $(BIN)/Pure;\
    1.27 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
    1.28 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
    1.29 +		  | $(COMP) $(BIN)/Pure;\
    1.30 +		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.31 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    1.32 +                  | $(COMP) $(BIN)/HOL;\
    1.33 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL;\
    1.34 +                fi;;\
    1.35 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.36 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    1.37 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' \
    1.38 +                       | $(BIN)/Pure;\
    1.39 +                fi;;\
    1.40  	*)	echo Bad value for ISABELLECOMP: \
    1.41                  	$(COMP) is not poly or sml; exit 1;;\
    1.42  	esac