make_html now only remains set if MAKE_HTML=true
authorclasohm
Sat Feb 10 19:04:21 1996 +0100 (1996-02-10)
changeset 149138a14548baad
parent 1490 713256365b92
child 1492 4e617b8f97ab
make_html now only remains set if MAKE_HTML=true
src/CCL/Makefile
src/CTT/Makefile
src/Cube/Makefile
src/FOL/Makefile
src/FOLP/Makefile
src/HOL/Makefile
src/HOLCF/Makefile
src/LCF/Makefile
src/LK/Makefile
src/Modal/Makefile
src/ZF/Makefile
     1.1 --- a/src/CCL/Makefile	Fri Feb 09 18:56:39 1996 +0100
     1.2 +++ b/src/CCL/Makefile	Sat Feb 10 19:04:21 1996 +0100
     1.3 @@ -36,14 +36,19 @@
     1.4  $(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)  $(CCL_FILES) 
     1.5  	case "$(COMP)" in \
     1.6  	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
     1.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     1.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     1.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    1.10                         | $(COMP) $(BIN)/CCL;\
    1.11 -		else echo 'open PolyML; exit_use_dir".";' \
    1.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CCL;\
    1.14 +                else echo 'open PolyML; exit_use_dir".";' \
    1.15                         | $(COMP) $(BIN)/CCL;\
    1.16                  fi;;\
    1.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.18 +	sml*)   if [ "$${MAKE_HTML}" = "true" ]; \
    1.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CCL" banner;' \
    1.22 +                       | $(BIN)/FOL;\
    1.23                  else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
    1.24                         | $(BIN)/FOL;\
    1.25                  fi;;\
    1.26 @@ -56,9 +61,16 @@
    1.27  
    1.28  test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
    1.29  	case "$(COMP)" in \
    1.30 -	poly*)	echo 'exit_use_dir"ex"; quit();' \
    1.31 -                  | $(COMP) $(BIN)/CCL ;;\
    1.32 -	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CCL;;\
    1.33 +	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.34 +                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    1.35 +                       | $(COMP) $(BIN)/CCL;\
    1.36 +                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CCL;\
    1.37 +                fi;;\
    1.38 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.39 +                then echo 'make_html := true; exit_use_dir"ex";' \
    1.40 +                       | $(BIN)/CCL;\
    1.41 +                else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
    1.42 +                fi;;\
    1.43  	*)	echo Bad value for ISABELLECOMP: \
    1.44                  	$(COMP) is not poly or sml;;\
    1.45  	esac
     2.1 --- a/src/CTT/Makefile	Fri Feb 09 18:56:39 1996 +0100
     2.2 +++ b/src/CTT/Makefile	Sat Feb 10 19:04:21 1996 +0100
     2.3 @@ -35,14 +35,19 @@
     2.4  	case "$(COMP)" in \
     2.5  	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
     2.6  			| $(COMP) $(BIN)/Pure;\
     2.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     2.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     2.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    2.10                         | $(COMP) $(BIN)/CTT;\
    2.11 -		else echo 'open PolyML; exit_use_dir".";' \
    2.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CTT;\
    2.14 +                else echo 'open PolyML; exit_use_dir".";' \
    2.15                         | $(COMP) $(BIN)/CTT;\
    2.16                  fi;;\
    2.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    2.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    2.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    2.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    2.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CTT" banner;' \
    2.22 +                       | $(BIN)/Pure;\
    2.23                  else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
    2.24                         | $(BIN)/Pure;\
    2.25                  fi;;\
     3.1 --- a/src/Cube/Makefile	Fri Feb 09 18:56:39 1996 +0100
     3.2 +++ b/src/Cube/Makefile	Sat Feb 10 19:04:21 1996 +0100
     3.3 @@ -28,14 +28,19 @@
     3.4  	case "$(COMP)" in \
     3.5  	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
     3.6  			| $(COMP) $(BIN)/Pure;\
     3.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     3.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     3.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    3.10                         | $(COMP) $(BIN)/Cube;\
    3.11 -		else echo 'open PolyML; exit_use_dir".";' \
    3.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    3.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Cube;\
    3.14 +                else echo 'open PolyML; exit_use_dir".";' \
    3.15  		       | $(COMP) $(BIN)/Cube;\
    3.16                  fi;;\
    3.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    3.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    3.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Cube" banner;' \
    3.22 +                       | $(BIN)/Pure;\
    3.23                  else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
    3.24                         | $(BIN)/Pure;\
    3.25                  fi;;\
     4.1 --- a/src/FOL/Makefile	Fri Feb 09 18:56:39 1996 +0100
     4.2 +++ b/src/FOL/Makefile	Sat Feb 10 19:04:21 1996 +0100
     4.3 @@ -39,14 +39,19 @@
     4.4  	case "$(COMP)" in \
     4.5  	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
     4.6  		  | $(COMP) $(BIN)/Pure;\
     4.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     4.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     4.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    4.10                         | $(COMP) $(BIN)/FOL;\
    4.11 -		else echo 'open PolyML; exit_use_dir".";' \
    4.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOL;\
    4.14 +                else echo 'open PolyML; exit_use_dir".";' \
    4.15                         | $(COMP) $(BIN)/FOL;\
    4.16                  fi;;\
    4.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    4.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    4.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    4.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    4.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOL" banner;' \
    4.22 +                       | $(BIN)/Pure;\
    4.23                  else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
    4.24                         | $(BIN)/Pure;\
    4.25                  fi;;\
    4.26 @@ -59,8 +64,16 @@
    4.27  
    4.28  test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
    4.29  	case "$(COMP)" in \
    4.30 -	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL ;;\
    4.31 -	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOL;;\
    4.32 +	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.33 +                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    4.34 +                       | $(COMP) $(BIN)/FOL;\
    4.35 +                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
    4.36 +                fi;;\
    4.37 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.38 +                then echo 'make_html := true; exit_use_dir"ex";' \
    4.39 +                       | $(BIN)/FOL;\
    4.40 +                else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
    4.41 +                fi;;\
    4.42  	*)	echo Bad value for ISABELLECOMP: \
    4.43                  	$(COMP) is not poly or sml;;\
    4.44  	esac
     5.1 --- a/src/FOLP/Makefile	Fri Feb 09 18:56:39 1996 +0100
     5.2 +++ b/src/FOLP/Makefile	Sat Feb 10 19:04:21 1996 +0100
     5.3 @@ -32,14 +32,19 @@
     5.4  	case "$(COMP)" in \
     5.5  	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
     5.6  			| $(COMP) $(BIN)/Pure;\
     5.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     5.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     5.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    5.10                         | $(COMP) $(BIN)/FOLP;\
    5.11 -		else echo 'open PolyML; exit_use_dir".";' \
    5.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOLP;\
    5.14 +                else echo 'open PolyML; exit_use_dir".";' \
    5.15  		       | $(COMP) $(BIN)/FOLP;\
    5.16                  fi;;\
    5.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    5.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    5.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOLP" banner;' \
    5.22 +                       | $(BIN)/Pure;\
    5.23                  else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    5.24                         | $(BIN)/Pure;\
    5.25                  fi;;\
    5.26 @@ -52,8 +57,16 @@
    5.27  
    5.28  test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
    5.29  	case "$(COMP)" in \
    5.30 -	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP ;;\
    5.31 -	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOLP;;\
    5.32 +	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.33 +                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    5.34 +                       | $(COMP) $(BIN)/FOLP;\
    5.35 +                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
    5.36 +                fi;;\
    5.37 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.38 +                then echo 'make_html := true; exit_use_dir"ex";' \
    5.39 +                       | $(BIN)/FOLP;\
    5.40 +                else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
    5.41 +                fi;;\
    5.42  	*)	echo Bad value for ISABELLECOMP: \
    5.43                  	$(COMP) is not poly or sml;;\
    5.44  	esac
     6.1 --- a/src/HOL/Makefile	Fri Feb 09 18:56:39 1996 +0100
     6.2 +++ b/src/HOL/Makefile	Sat Feb 10 19:04:21 1996 +0100
     6.3 @@ -40,14 +40,19 @@
     6.4  	case "$(COMP)" in \
     6.5  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
     6.6  		  | $(COMP) $(BIN)/Pure;\
     6.7 -		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     6.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     6.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    6.10 -                  | $(COMP) $(BIN)/HOL;\
    6.11 -		else echo 'open PolyML; exit_use_dir".";' \
    6.12 +                       | $(COMP) $(BIN)/HOL;\
    6.13 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.14 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
    6.15 +                else echo 'open PolyML; exit_use_dir".";' \
    6.16                         | $(COMP) $(BIN)/HOL;\
    6.17                  fi;;\
    6.18 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    6.19 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    6.20                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    6.21 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    6.22 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOL" banner;' \
    6.23 +                       | $(BIN)/Pure;\
    6.24                  else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    6.25                         | $(BIN)/Pure;\
    6.26                  fi;;\
    6.27 @@ -73,14 +78,21 @@
    6.28  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    6.29  
    6.30  IMP:    $(BIN)/HOL  $(IMP_FILES)
    6.31 -	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
    6.32 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.33 +        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    6.34 +        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
    6.35 +        fi
    6.36  
    6.37  ##Hoare logic
    6.38  Hoare_NAMES = Hoare Arith2 Examples
    6.39 -Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
    6.40 +Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
    6.41 +              $(Hoare_NAMES:%=Hoare/%.ML)
    6.42  
    6.43  Hoare:  $(BIN)/HOL  $(Hoare_FILES)
    6.44 -	echo 'exit_use_dir"Hoare";quit();' | $(LOGIC)
    6.45 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.46 +        then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
    6.47 +        else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
    6.48 +        fi
    6.49  
    6.50  ##The integers in HOL
    6.51  INTEG_NAMES = Equiv Integ 
    6.52 @@ -89,7 +101,10 @@
    6.53                $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    6.54  
    6.55  Integ:  $(BIN)/HOL  $(INTEG_FILES)
    6.56 -	echo 'exit_use_dir"Integ";quit();' | $(LOGIC)
    6.57 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.58 +        then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
    6.59 +        else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
    6.60 +        fi
    6.61  
    6.62  ##I/O Automata
    6.63  IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
    6.64 @@ -106,8 +121,14 @@
    6.65   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    6.66  
    6.67  IOA:    $(BIN)/HOL  $(IOA_FILES)
    6.68 -	echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC)
    6.69 -	echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC)
    6.70 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.71 +        then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
    6.72 +               | $(LOGIC);\
    6.73 +             echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
    6.74 +               | $(LOGIC);\
    6.75 +        else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
    6.76 +	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
    6.77 +        fi
    6.78  
    6.79  ##Properties of substitutions
    6.80  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    6.81 @@ -116,7 +137,10 @@
    6.82                $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    6.83  
    6.84  Subst:  $(BIN)/HOL  $(SUBST_FILES)
    6.85 -	echo 'exit_use_dir"Subst";quit();' | $(LOGIC)
    6.86 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.87 +        then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
    6.88 +        else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
    6.89 +        fi
    6.90  
    6.91  ##Confluence of Lambda-calculus
    6.92  LAMBDA_NAMES = Lambda ParRed Commutation Eta
    6.93 @@ -125,7 +149,11 @@
    6.94                $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    6.95  
    6.96  Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
    6.97 -	echo 'exit_use_dir"Lambda";quit();' | $(LOGIC)
    6.98 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.99 +        then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   6.100 +               | $(LOGIC);\
   6.101 +        else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   6.102 +        fi
   6.103  
   6.104  ##Type inference for MiniML
   6.105  MINIML_NAMES = I Maybe MiniML Type W
   6.106 @@ -134,7 +162,11 @@
   6.107                $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   6.108  
   6.109  MiniML: $(BIN)/HOL  $(MINIML_FILES)
   6.110 -	echo 'exit_use_dir"MiniML";quit();' | $(LOGIC)
   6.111 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.112 +        then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   6.113 +               | $(LOGIC);\
   6.114 +        else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   6.115 +        fi
   6.116  
   6.117  ##Lexical analysis
   6.118  LEX_FILES = Auto AutoChopper Chopper Prefix
   6.119 @@ -143,7 +175,10 @@
   6.120              $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   6.121  
   6.122  Lex:	$(BIN)/HOL  $(LEX_FILES)
   6.123 -	echo 'exit_use_dir"Lex";quit();' | $(LOGIC)
   6.124 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.125 +        then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   6.126 +        else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   6.127 +        fi
   6.128  
   6.129  ##Miscellaneous examples
   6.130  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
   6.131 @@ -153,7 +188,10 @@
   6.132             ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   6.133  
   6.134  ex:     $(BIN)/HOL  $(EX_FILES)
   6.135 -	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
   6.136 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.137 +        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   6.138 +        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   6.139 +        fi
   6.140  
   6.141  #Full test.
   6.142  test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
     7.1 --- a/src/HOLCF/Makefile	Fri Feb 09 18:56:39 1996 +0100
     7.2 +++ b/src/HOLCF/Makefile	Sat Feb 10 19:04:21 1996 +0100
     7.3 @@ -36,14 +36,19 @@
     7.4  $(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
     7.5  	case "$(COMP)" in \
     7.6  	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
     7.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     7.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     7.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    7.10                         | $(COMP) $(BIN)/HOLCF;\
    7.11 -		else echo 'open PolyML; exit_use_dir".";' \
    7.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOLCF;\
    7.14 +                else echo 'open PolyML; exit_use_dir".";' \
    7.15  		       | $(COMP) $(BIN)/HOLCF;\
    7.16                  fi;;\
    7.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    7.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    7.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    7.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    7.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOLCF" banner;' \
    7.22 +                       | $(BIN)/HOL;\
    7.23                  else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
    7.24                         | $(BIN)/HOL;\
    7.25                  fi;;\
    7.26 @@ -61,8 +66,16 @@
    7.27  
    7.28  test:   ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
    7.29  	case "$(COMP)" in \
    7.30 -	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
    7.31 -	sml*)	echo 'exit_use_dir"ex"' | $(BIN)/HOLCF;;\
    7.32 +	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.33 +                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    7.34 +                       | $(COMP) $(BIN)/HOLCF;\
    7.35 +                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
    7.36 +                fi;;\
    7.37 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.38 +                then echo 'make_html := true; exit_use_dir"ex";' \
    7.39 +                       | $(BIN)/HOLCF;\
    7.40 +                else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
    7.41 +                fi;;\
    7.42  	*)	echo Bad value for ISABELLECOMP: \
    7.43                  	$(COMP) is not poly or sml;;\
    7.44  	esac
    7.45 @@ -77,9 +90,16 @@
    7.46  
    7.47  test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
    7.48  	case "$(COMP)" in \
    7.49 -	poly*)	echo 'exit_use_dir"explicit_domains"; quit();' \
    7.50 -                  | $(COMP) $(BIN)/HOLCF ;;\
    7.51 -	sml*)	echo 'exit_use_dir"explicit_domains"' | $(BIN)/HOLCF;;\
    7.52 +	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.53 +                then echo 'make_html := true; exit_use_dir"explicit_domains";                             quit();' | $(COMP) $(BIN)/HOLCF;\
    7.54 +                else echo 'exit_use_dir"explicit_domains"; quit();' \
    7.55 +                       | $(COMP) $(BIN)/HOLCF;\
    7.56 +                fi;;\
    7.57 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.58 +                then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
    7.59 +                       | $(BIN)/HOLCF;\
    7.60 +                else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
    7.61 +                fi;;\
    7.62  	*)	echo Bad value for ISABELLECOMP: \
    7.63                  	$(COMP) is not poly or sml;;\
    7.64  	esac
     8.1 --- a/src/LCF/Makefile	Fri Feb 09 18:56:39 1996 +0100
     8.2 +++ b/src/LCF/Makefile	Sat Feb 10 19:04:21 1996 +0100
     8.3 @@ -27,14 +27,19 @@
     8.4  $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
     8.5  	case "$(COMP)" in \
     8.6  	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
     8.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     8.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     8.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    8.10                         | $(COMP) $(BIN)/LCF;\
    8.11 -		else echo 'open PolyML; exit_use_dir".";' \
    8.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    8.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LCF;\
    8.14 +                else echo 'open PolyML; exit_use_dir".";' \
    8.15                         | $(COMP) $(BIN)/LCF;\
    8.16                  fi;;\
    8.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    8.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    8.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
    8.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    8.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/LCF" banner;' \
    8.22 +                       | $(BIN)/FOL;\
    8.23                  else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
    8.24                         | $(BIN)/FOL;\
    8.25                  fi;;\
     9.1 --- a/src/LK/Makefile	Fri Feb 09 18:56:39 1996 +0100
     9.2 +++ b/src/LK/Makefile	Sat Feb 10 19:04:21 1996 +0100
     9.3 @@ -28,13 +28,18 @@
     9.4  	case "$(COMP)" in \
     9.5  	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
     9.6  			| $(COMP) $(BIN)/Pure;\
     9.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     9.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
     9.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    9.10                         | $(COMP) $(BIN)/LK;\
    9.11 -		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
    9.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    9.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LK;\
    9.14 +                else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
    9.15                  fi;;\
    9.16 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    9.17 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    9.18                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
    9.19 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    9.20 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/LK" banner;' \
    9.21 +                       | $(BIN)/Pure;\
    9.22                  else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
    9.23                         | $(BIN)/Pure;\
    9.24                  fi;;\
    10.1 --- a/src/Modal/Makefile	Fri Feb 09 18:56:39 1996 +0100
    10.2 +++ b/src/Modal/Makefile	Sat Feb 10 19:04:21 1996 +0100
    10.3 @@ -28,14 +28,19 @@
    10.4  $(BIN)/Modal:   $(BIN)/LK  $(FILES) 
    10.5  	case "$(COMP)" in \
    10.6  	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
    10.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    10.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
    10.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   10.10                         | $(COMP) $(BIN)/Modal;\
   10.11 -		else echo 'open PolyML; exit_use_dir".";' \
   10.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   10.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Modal;\
   10.14 +                else echo 'open PolyML; exit_use_dir".";' \
   10.15  		       | $(COMP) $(BIN)/Modal;\
   10.16                  fi;;\
   10.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   10.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   10.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
   10.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   10.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Modal" banner;' \
   10.22 +                       | $(BIN)/LK;\
   10.23                  else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
   10.24                         | $(BIN)/LK;\
   10.25                  fi;;\
    11.1 --- a/src/ZF/Makefile	Fri Feb 09 18:56:39 1996 +0100
    11.2 +++ b/src/ZF/Makefile	Sat Feb 10 19:04:21 1996 +0100
    11.3 @@ -37,13 +37,19 @@
    11.4  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    11.5  	case "$(COMP)" in \
    11.6  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
    11.7 -                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    11.8 +                if [ "$${MAKE_HTML}" = "true" ]; \
    11.9                  then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   11.10                         | $(COMP) $(BIN)/ZF;\
   11.11 -		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/ZF;\
   11.12 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.13 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
   11.14 +                else echo 'open PolyML; exit_use_dir".";' \
   11.15 +                       | $(COMP) $(BIN)/ZF;\
   11.16                  fi;;\
   11.17 -	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   11.18 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   11.19                  then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   11.20 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   11.21 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/ZF" banner;' \
   11.22 +                       | $(BIN)/FOL;\
   11.23                  else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
   11.24                         | $(BIN)/FOL;\
   11.25                  fi;;\
   11.26 @@ -69,7 +75,10 @@
   11.27  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
   11.28  
   11.29  IMP:   $(BIN)/ZF  $(IMP_FILES)
   11.30 -	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
   11.31 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.32 +        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.33 +        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.34 +        fi
   11.35  
   11.36  ##Coinduction example
   11.37  COIND_NAMES = ECR Language MT Map Static Types Values 
   11.38 @@ -78,7 +87,10 @@
   11.39                $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
   11.40  
   11.41  Coind:  $(BIN)/ZF  $(COIND_FILES)
   11.42 -	echo 'exit_use_dir"Coind";quit();' | $(LOGIC)
   11.43 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.44 +        then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
   11.45 +        else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
   11.46 +        fi
   11.47  
   11.48  ##AC examples
   11.49  AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
   11.50 @@ -92,7 +104,10 @@
   11.51             $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
   11.52  
   11.53  AC:  $(BIN)/ZF  $(AC_FILES)
   11.54 -	echo 'exit_use_dir"AC";quit();' | $(LOGIC)
   11.55 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.56 +        then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
   11.57 +        else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
   11.58 +        fi
   11.59  
   11.60  ##Residuals example
   11.61  
   11.62 @@ -103,7 +118,10 @@
   11.63                              $(RESID_NAMES:%=Resid/%.ML)
   11.64  
   11.65  Resid:  $(BIN)/ZF  $(RESID_FILES)
   11.66 -	echo 'exit_use_dir"Resid";quit();' | $(LOGIC)
   11.67 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.68 +        then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
   11.69 +        else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
   11.70 +        fi
   11.71  
   11.72  ##Miscellaneous examples
   11.73  EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
   11.74 @@ -113,7 +131,10 @@
   11.75  
   11.76  #Test ZF by loading the examples in directory ex
   11.77  ex:     $(BIN)/ZF  $(EX_FILES)
   11.78 -	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
   11.79 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.80 +        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
   11.81 +        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   11.82 +        fi
   11.83  
   11.84  #Full test.
   11.85  test:   $(BIN)/ZF IMP Coind AC Resid ex