src/HOL/Makefile
changeset 2117 292df12bace5
parent 2094 2061df98aab5
child 2235 866dbb04816c
     1.1 --- a/src/HOL/Makefile	Mon Oct 21 09:51:18 1996 +0200
     1.2 +++ b/src/HOL/Makefile	Mon Oct 21 11:18:34 1996 +0200
     1.3 @@ -33,12 +33,12 @@
     1.4  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
     1.5  
     1.6  $(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
     1.7 -	if [ -d $${ISABELLEBIN:?}/Pure ];\
     1.8 +	@if [ -d $${ISABELLEBIN:?}/Pure ];\
     1.9  		then echo Bad value for ISABELLEBIN: \
    1.10  			$(BIN) is the Isabelle source directory; \
    1.11  			exit 1; \
    1.12 -		fi;\
    1.13 -	case "$(COMP)" in \
    1.14 +	fi
    1.15 +	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
    1.16  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
    1.17  		  | $(COMP) $(BIN)/Pure;\
    1.18  		if [ "$${MAKE_HTML}" = "true" ]; \
    1.19 @@ -59,7 +59,7 @@
    1.20  		       | $(BIN)/Pure;\
    1.21  		fi;;\
    1.22  	*)	echo Bad value for ISABELLECOMP: \
    1.23 -			$(COMP) is not poly or sml; exit 1;;\
    1.24 +			\"$(COMP)\" is not poly or sml; exit 1;;\
    1.25  	esac
    1.26  
    1.27  $(BIN)/Pure:
    1.28 @@ -68,11 +68,11 @@
    1.29  #### Testing of HOL
    1.30  
    1.31  #A macro referring to the object-logic (depends on ML compiler)
    1.32 -LOGIC:sh=case $ISABELLECOMP in \
    1.33 +LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
    1.34  	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
    1.35  	sml*)	echo "$ISABELLEBIN/HOL" ;;\
    1.36 -	*)	echo "echo Bad value for ISABELLECOMP: \
    1.37 -			$ISABELLEBIN is not poly or sml; exit 1" ;;\
    1.38 +	*)	echo "echo; echo Bad value for ISABELLECOMP: \
    1.39 +			$ISABELLECOMP is not poly or sml; exit 1" ;;\
    1.40  	esac
    1.41  
    1.42  ##IMP-semantics example
    1.43 @@ -80,7 +80,7 @@
    1.44  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.45  
    1.46  IMP:	$(BIN)/HOL  $(IMP_FILES)
    1.47 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.48 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.49  	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    1.50  	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
    1.51  	fi
    1.52 @@ -91,7 +91,7 @@
    1.53  	      $(Hoare_NAMES:%=Hoare/%.ML)
    1.54  
    1.55  Hoare:	$(BIN)/HOL  $(Hoare_FILES)
    1.56 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.57 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.58  	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
    1.59  	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
    1.60  	fi
    1.61 @@ -103,7 +103,7 @@
    1.62  	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.63  
    1.64  Integ:	$(BIN)/HOL  $(INTEG_FILES)
    1.65 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.66 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.67  	then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
    1.68  	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
    1.69  	fi
    1.70 @@ -123,7 +123,7 @@
    1.71   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.72  
    1.73  IOA:	$(BIN)/HOL  $(IOA_FILES)
    1.74 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.75 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.76  	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
    1.77  	       | $(LOGIC);\
    1.78  	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
    1.79 @@ -134,12 +134,13 @@
    1.80  
    1.81  
    1.82  ##Authentication & Security Protocols
    1.83 -Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
    1.84 +Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
    1.85 +	     Yahalom Yahalom2
    1.86  
    1.87  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    1.88  
    1.89  Auth:	$(BIN)/HOL  $(AUTH_FILES)
    1.90 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.91 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.92  	then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
    1.93  	else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
    1.94  	fi
    1.95 @@ -152,7 +153,7 @@
    1.96  	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.97  
    1.98  Subst:	$(BIN)/HOL  $(SUBST_FILES)
    1.99 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.100 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.101  	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
   1.102  	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
   1.103  	fi
   1.104 @@ -164,7 +165,7 @@
   1.105  	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   1.106  
   1.107  Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
   1.108 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.109 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.110  	then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   1.111  	       | $(LOGIC);\
   1.112  	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   1.113 @@ -177,7 +178,7 @@
   1.114  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   1.115  
   1.116  MiniML: $(BIN)/HOL  $(MINIML_FILES)
   1.117 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.118 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.119  	then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   1.120  	       | $(LOGIC);\
   1.121  	else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   1.122 @@ -190,7 +191,7 @@
   1.123  	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   1.124  
   1.125  Lex:	$(BIN)/HOL  $(LEX_FILES)
   1.126 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.127 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.128  	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   1.129  	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   1.130  	fi
   1.131 @@ -203,7 +204,7 @@
   1.132  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.133  
   1.134  ex:	$(BIN)/HOL  $(EX_FILES)
   1.135 -	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.136 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.137  	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   1.138  	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   1.139  	fi