added calls of init_html and make_chart
authorclasohm
Tue Oct 24 14:50:24 1995 +0100 (1995-10-24)
changeset 1296ae31bb7774a7
parent 1295 27c1e88a62b4
child 1297 7ac266cf82d0
added calls of init_html and make_chart
src/Cube/Makefile
src/Cube/ROOT.ML
src/FOL/Makefile
src/FOL/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/Makefile
src/FOLP/ROOT.ML
src/FOLP/ex/ROOT.ML
src/HOL/AxClasses/Group/ROOT.ML
src/HOL/AxClasses/Tutorial/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/Integ/ROOT.ML
src/HOL/Lambda/ROOT.ML
src/HOL/Makefile
src/HOL/ROOT.ML
src/HOL/Subst/ROOT.ML
src/HOL/ex/ROOT.ML
src/LCF/Makefile
src/LCF/ROOT.ML
src/Modal/Makefile
src/Modal/ROOT.ML
src/Modal/ex/ROOT.ML
src/ZF/AC/ROOT.ML
src/ZF/Coind/ROOT.ML
src/ZF/IMP/ROOT.ML
src/ZF/Makefile
src/ZF/ROOT.ML
src/ZF/Resid/ROOT.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/src/Cube/Makefile	Tue Oct 24 14:49:45 1995 +0100
     1.2 +++ b/src/Cube/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 (Cube)			#
     1.8 @@ -8,6 +9,8 @@
     1.9  #	make 
    1.10  #To make the system and test it on standard examples, type  
    1.11  #	make test
    1.12 +#To generate HTML files for every theory, set the environment variable
    1.13 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    1.14  
    1.15  #Environment variable ISABELLECOMP specifies the compiler.
    1.16  #Environment variable ISABELLEBIN specifies the destination directory.
    1.17 @@ -25,8 +28,17 @@
    1.18  	case "$(COMP)" in \
    1.19  	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
    1.20  			| $(COMP) $(BIN)/Pure;\
    1.21 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Cube ;;\
    1.22 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' | $(BIN)/Pure ;;\
    1.23 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.24 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    1.25 +                       | $(COMP) $(BIN)/Cube;\
    1.26 +		else echo 'open PolyML; exit_use"ROOT";' \
    1.27 +		       | $(COMP) $(BIN)/Cube;\
    1.28 +                fi;;\
    1.29 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.30 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    1.31 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' \
    1.32 +                       | $(BIN)/Pure;\
    1.33 +                fi;;\
    1.34  	*)	echo Bad value for ISABELLECOMP: \
    1.35                  	$(COMP) is not poly or sml;;\
    1.36  	esac
     2.1 --- a/src/Cube/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     2.2 +++ b/src/Cube/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     2.3 @@ -17,4 +17,6 @@
     2.4  use "../Pure/install_pp.ML";
     2.5  print_depth 8;
     2.6  
     2.7 +make_chart ();   (*make HTML chart*)
     2.8 +
     2.9  val Cube_build_completed = ();	(*indicate successful build*)
     3.1 --- a/src/FOL/Makefile	Tue Oct 24 14:49:45 1995 +0100
     3.2 +++ b/src/FOL/Makefile	Tue Oct 24 14:50:24 1995 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -#  $Id$
     3.5 +# $Id$
     3.6  #########################################################################
     3.7  #									#
     3.8  # 			Makefile for Isabelle (FOL)			#
     3.9 @@ -6,9 +6,11 @@
    3.10  #########################################################################
    3.11  
    3.12  #To make the system, cd to this directory and type  
    3.13 -#	make -f Makefile 
    3.14 +#	make
    3.15  #To make the system and test it on standard examples, type  
    3.16 -#	make -f Makefile test
    3.17 +#	make test
    3.18 +#To generate HTML files for every theory, set the environment variable
    3.19 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    3.20  
    3.21  #Environment variable ISABELLECOMP specifies the compiler.
    3.22  #Environment variable ISABELLEBIN specifies the destination directory.
    3.23 @@ -35,10 +37,18 @@
    3.24                  	exit 1; \
    3.25             	fi;\
    3.26  	case "$(COMP)" in \
    3.27 -	poly*)	echo 'make_database"$(BIN)/FOL"; quit();'  \
    3.28 -			| $(COMP) $(BIN)/Pure;\
    3.29 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOL;;\
    3.30 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;;\
    3.31 +	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
    3.32 +		  | $(COMP) $(BIN)/Pure;\
    3.33 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    3.34 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    3.35 +                       | $(COMP) $(BIN)/FOL;\
    3.36 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOL;\
    3.37 +                fi;;\
    3.38 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.39 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    3.40 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOL" banner;' \
    3.41 +                       | $(BIN)/Pure;\
    3.42 +                fi;;\
    3.43  	*)	echo Bad value for ISABELLECOMP: \
    3.44                  	$(COMP) is not poly or sml;;\
    3.45  	esac
     4.1 --- a/src/FOL/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     4.2 +++ b/src/FOL/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     4.3 @@ -72,5 +72,6 @@
     4.4  use "../Pure/install_pp.ML";
     4.5  print_depth 8;
     4.6  
     4.7 +make_chart ();   (*make HTML chart*)
     4.8 +
     4.9  val FOL_build_completed = ();	(*indicate successful build*)
    4.10 -
     5.1 --- a/src/FOL/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     5.2 +++ b/src/FOL/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     5.3 @@ -37,4 +37,6 @@
     5.4  time_use_thy "ex/Nat2";
     5.5  time_use_thy "ex/List";
     5.6  
     5.7 +make_chart ();   (*make HTML chart*)
     5.8 +
     5.9  maketest"END: Root file for FOL examples";
     6.1 --- a/src/FOLP/Makefile	Tue Oct 24 14:49:45 1995 +0100
     6.2 +++ b/src/FOLP/Makefile	Tue Oct 24 14:50:24 1995 +0100
     6.3 @@ -6,9 +6,11 @@
     6.4  #########################################################################
     6.5  
     6.6  #To make the system, cd to this directory and type  
     6.7 -#	make -f Makefile 
     6.8 +#	make
     6.9  #To make the system and test it on standard examples, type  
    6.10 -#	make -f Makefile test
    6.11 +#	make test
    6.12 +#To generate HTML files for every theory, set the environment variable
    6.13 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    6.14  
    6.15  #Environment variable ISABELLECOMP specifies the compiler.
    6.16  #Environment variable ISABELLEBIN specifies the destination directory.
    6.17 @@ -30,8 +32,17 @@
    6.18  	case "$(COMP)" in \
    6.19  	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    6.20  			| $(COMP) $(BIN)/Pure;\
    6.21 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/FOLP;;\
    6.22 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;;\
    6.23 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.24 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    6.25 +                       | $(COMP) $(BIN)/FOLP;\
    6.26 +		else echo 'open PolyML; exit_use"ROOT";' \
    6.27 +		       | $(COMP) $(BIN)/FOLP;\
    6.28 +                fi;;\
    6.29 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    6.30 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    6.31 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' \
    6.32 +                       | $(BIN)/Pure;\
    6.33 +                fi;;\
    6.34  	*)	echo Bad value for ISABELLECOMP: \
    6.35                  	$(COMP) is not poly or sml;;\
    6.36  	esac
     7.1 --- a/src/FOLP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     7.2 +++ b/src/FOLP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     7.3 @@ -78,4 +78,6 @@
     7.4  use "../Pure/install_pp.ML";
     7.5  print_depth 8;
     7.6  
     7.7 +make_chart ();   (*make HTML chart*)
     7.8 +
     7.9  val FOLP_build_completed = ();	(*indicate successful build*)
     8.1 --- a/src/FOLP/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     8.2 +++ b/src/FOLP/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     8.3 @@ -32,4 +32,6 @@
     8.4  time_use     "ex/prop.ML";
     8.5  time_use     "ex/quant.ML";
     8.6  
     8.7 +make_chart ();   (*make HTML chart*)
     8.8 +
     8.9  maketest"END: Root file for FOLP examples";
     9.1 --- a/src/HOL/AxClasses/Group/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
     9.2 +++ b/src/HOL/AxClasses/Group/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
     9.3 @@ -25,3 +25,5 @@
     9.4  
     9.5  use_thy "GroupDefs";
     9.6  use_thy "GroupInsts";
     9.7 +
     9.8 +make_chart ();   (*make HTML chart*)
    10.1 --- a/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    10.2 +++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    10.3 @@ -33,3 +33,5 @@
    10.4  
    10.5  use_thy "Product";
    10.6  use_thy "ProductInsts";
    10.7 +
    10.8 +make_chart ();   (*make HTML chart*)
    11.1 --- a/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    11.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    11.3 @@ -22,3 +22,5 @@
    11.4  time_use_thy "Properties";
    11.5  time_use_thy "Equiv";
    11.6  time_use_thy "Hoare";
    11.7 +
    11.8 +make_chart ();   (*make HTML chart*)
    12.1 --- a/src/HOL/Integ/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    12.2 +++ b/src/HOL/Integ/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    12.3 @@ -10,3 +10,5 @@
    12.4  
    12.5  loadpath := ["Integ"];
    12.6  time_use_thy "Integ";
    12.7 +
    12.8 +make_chart ();   (*make HTML chart*)
    13.1 --- a/src/HOL/Lambda/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    13.2 +++ b/src/HOL/Lambda/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    13.3 @@ -19,4 +19,7 @@
    13.4  
    13.5  writeln"Root file for HOL/Lambda";
    13.6  loadpath := [".","Lambda"];
    13.7 +
    13.8  time_use_thy "Eta";
    13.9 +
   13.10 +make_chart ();   (*make HTML chart*)
    14.1 --- a/src/HOL/Makefile	Tue Oct 24 14:49:45 1995 +0100
    14.2 +++ b/src/HOL/Makefile	Tue Oct 24 14:50:24 1995 +0100
    14.3 @@ -1,3 +1,4 @@
    14.4 +# $Id$
    14.5  #########################################################################
    14.6  #									#
    14.7  # 			Makefile for Isabelle (HOL)			#
    14.8 @@ -5,9 +6,11 @@
    14.9  #########################################################################
   14.10  
   14.11  #To make the system, cd to this directory and type  
   14.12 -#	make -f Makefile 
   14.13 +#	make
   14.14  #To make the system and test it on standard examples, type  
   14.15 -#	make -f Makefile test
   14.16 +#	make test
   14.17 +#To generate HTML files for every theory, set the environment variable
   14.18 +#MAKE_HTML or add the parameter "MAKE_HTML=".
   14.19  
   14.20  #Environment variable ISABELLECOMP specifies the compiler.
   14.21  #Environment variable ISABELLEBIN specifies the destination directory.
   14.22 @@ -36,9 +39,17 @@
   14.23             	fi;\
   14.24  	case "$(COMP)" in \
   14.25  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
   14.26 -			| $(COMP) $(BIN)/Pure;\
   14.27 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
   14.28 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
   14.29 +		  | $(COMP) $(BIN)/Pure;\
   14.30 +		if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   14.31 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
   14.32 +                  | $(COMP) $(BIN)/HOL;\
   14.33 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL;\
   14.34 +                fi;;\
   14.35 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   14.36 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
   14.37 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' \
   14.38 +                       | $(BIN)/Pure;\
   14.39 +                fi;;\
   14.40  	*)	echo Bad value for ISABELLECOMP: \
   14.41                  	$(COMP) is not poly or sml; exit 1;;\
   14.42  	esac
    15.1 --- a/src/HOL/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    15.2 +++ b/src/HOL/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    15.3 @@ -85,4 +85,6 @@
    15.4  init_pps ();
    15.5  print_depth 8;
    15.6  
    15.7 +make_chart ();   (*make HTML chart*)
    15.8 +
    15.9  val HOL_build_completed = ();   (*indicate successful build*)
    16.1 --- a/src/HOL/Subst/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    16.2 +++ b/src/HOL/Subst/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    16.3 @@ -30,4 +30,6 @@
    16.4  
    16.5  use_thy "Unifier";
    16.6  
    16.7 +make_chart ();   (*make HTML chart*)
    16.8 +
    16.9  writeln"END: Root file for Substitutions and Unification";
    17.1 --- a/src/HOL/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    17.2 +++ b/src/HOL/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    17.3 @@ -30,4 +30,7 @@
    17.4  time_use_thy "Term";
    17.5  time_use_thy "Simult";
    17.6  time_use_thy "MT";
    17.7 +
    17.8 +make_chart ();   (*make HTML chart*)
    17.9 +
   17.10  writeln "END: Root file for HOL examples";
    18.1 --- a/src/LCF/Makefile	Tue Oct 24 14:49:45 1995 +0100
    18.2 +++ b/src/LCF/Makefile	Tue Oct 24 14:50:24 1995 +0100
    18.3 @@ -1,3 +1,4 @@
    18.4 +# $Id$
    18.5  #########################################################################
    18.6  #									#
    18.7  # 			Makefile for Isabelle (LCF)			#
    18.8 @@ -8,6 +9,8 @@
    18.9  #	make 
   18.10  #To make the system and test it on standard examples, type  
   18.11  #	make test
   18.12 +#To generate HTML files for every theory, set the environment variable
   18.13 +#MAKE_HTML or add the parameter "MAKE_HTML=".
   18.14  
   18.15  #Environment variable ISABELLECOMP specifies the compiler.
   18.16  #Environment variable ISABELLEBIN specifies the destination directory.
   18.17 @@ -24,8 +27,16 @@
   18.18  $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
   18.19  	case "$(COMP)" in \
   18.20  	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
   18.21 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF ;;\
   18.22 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;;\
   18.23 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   18.24 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
   18.25 +                       | $(COMP) $(BIN)/LCF;\
   18.26 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF;\
   18.27 +                fi;;\
   18.28 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   18.29 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
   18.30 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' \
   18.31 +                       | $(BIN)/FOL;\
   18.32 +                fi;;\
   18.33  	*)	echo Bad value for ISABELLECOMP: \
   18.34                  	$(COMP) is not poly or sml;;\
   18.35  	esac
    19.1 --- a/src/LCF/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    19.2 +++ b/src/LCF/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    19.3 @@ -17,4 +17,6 @@
    19.4  use"pair.ML";
    19.5  use"fix.ML";
    19.6  
    19.7 +make_chart ();   (*make HTML chart*)
    19.8 +
    19.9  val LCF_build_completed = ();	(*indicate successful build*)
    20.1 --- a/src/Modal/Makefile	Tue Oct 24 14:49:45 1995 +0100
    20.2 +++ b/src/Modal/Makefile	Tue Oct 24 14:50:24 1995 +0100
    20.3 @@ -1,3 +1,4 @@
    20.4 +# $Id$
    20.5  #########################################################################
    20.6  #									#
    20.7  # 			Makefile for Isabelle (Modal)			#
    20.8 @@ -5,9 +6,11 @@
    20.9  #########################################################################
   20.10  
   20.11  #To make the system, cd to this directory and type
   20.12 -#	make -f Makefile 
   20.13 +#	make
   20.14  #To make the system and test it on standard examples, type 
   20.15 -#	make -f Makefile test
   20.16 +#	make test
   20.17 +#To generate HTML files for every theory, set the environment variable
   20.18 +#MAKE_HTML or add the parameter "MAKE_HTML=".
   20.19  
   20.20  #Environment variable ISABELLECOMP specifies the compiler.
   20.21  #Environment variable ISABELLEBIN specifies the destination directory.
   20.22 @@ -25,8 +28,17 @@
   20.23  $(BIN)/Modal:   $(BIN)/LK  $(FILES) 
   20.24  	case "$(COMP)" in \
   20.25  	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
   20.26 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Modal ;;\
   20.27 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' | $(BIN)/LK;;\
   20.28 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   20.29 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
   20.30 +                       | $(COMP) $(BIN)/Modal;\
   20.31 +		else echo 'open PolyML; exit_use"ROOT";' \
   20.32 +		       | $(COMP) $(BIN)/Modal;\
   20.33 +                fi;;\
   20.34 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   20.35 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
   20.36 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' \
   20.37 +                       | $(BIN)/LK;\
   20.38 +                fi;;\
   20.39  	*)	echo Bad value for ISABELLECOMP: \
   20.40                  	$(COMP) is not poly or sml;;\
   20.41  	esac
    21.1 --- a/src/Modal/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    21.2 +++ b/src/Modal/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    21.3 @@ -78,6 +78,8 @@
    21.4  end;
    21.5  structure S43_Prover = Modal_ProverFun(MP_Rule);  
    21.6  
    21.7 +make_chart ();   (*make HTML chart*)
    21.8 +
    21.9  val Modal_build_completed = ();	(*indicate successful build*)
   21.10  
   21.11  (*printing functions are inherited from LK*)
    22.1 --- a/src/Modal/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    22.2 +++ b/src/Modal/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    22.3 @@ -25,4 +25,6 @@
    22.4  time_use "ex/S4thms.ML";
    22.5  time_use "ex/S43thms.ML";
    22.6  
    22.7 +make_chart ();   (*make HTML chart*)
    22.8 +
    22.9  maketest"END: Root file for Modal examples";
    23.1 --- a/src/ZF/AC/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    23.2 +++ b/src/ZF/AC/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    23.3 @@ -40,4 +40,6 @@
    23.4  
    23.5  time_use_thy "AC/DC";
    23.6  
    23.7 +make_chart ();   (*make HTML chart*)
    23.8 +
    23.9  writeln"END: Root file for ZF/AC";
    24.1 --- a/src/ZF/Coind/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    24.2 +++ b/src/ZF/Coind/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    24.3 @@ -19,3 +19,5 @@
    24.4  proof_timing := true;
    24.5  loadpath     := [".","Coind"];
    24.6  time_use_thy "MT";
    24.7 +
    24.8 +make_chart ();   (*make HTML chart*)
    25.1 --- a/src/ZF/IMP/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    25.2 +++ b/src/ZF/IMP/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    25.3 @@ -18,3 +18,5 @@
    25.4  proof_timing := true;
    25.5  loadpath := [".","IMP"];
    25.6  time_use_thy "Equiv";
    25.7 +
    25.8 +make_chart ();   (*make HTML chart*)
    26.1 --- a/src/ZF/Makefile	Tue Oct 24 14:49:45 1995 +0100
    26.2 +++ b/src/ZF/Makefile	Tue Oct 24 14:50:24 1995 +0100
    26.3 @@ -1,4 +1,4 @@
    26.4 -#  $Id$
    26.5 +# $Id$
    26.6  #########################################################################
    26.7  #									#
    26.8  # 			Makefile for Isabelle (ZF)			#
    26.9 @@ -6,9 +6,11 @@
   26.10  #########################################################################
   26.11  
   26.12  #To make the system, cd to this directory and type
   26.13 -#	make -f Makefile 
   26.14 +#	make
   26.15  #To make the system and test it on standard examples, type 
   26.16 -#	make -f Makefile test
   26.17 +#	make test
   26.18 +#To generate HTML files for every theory, set the environment variable
   26.19 +#MAKE_HTML or add the parameter "MAKE_HTML=".
   26.20  
   26.21  #Environment variable ISABELLECOMP specifies the compiler.
   26.22  #Environment variable ISABELLEBIN specifies the destination directory.
   26.23 @@ -35,8 +37,16 @@
   26.24  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
   26.25  	case "$(COMP)" in \
   26.26  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
   26.27 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
   26.28 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
   26.29 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   26.30 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
   26.31 +                       | $(COMP) $(BIN)/ZF;\
   26.32 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\
   26.33 +                fi;;\
   26.34 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   26.35 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   26.36 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' \
   26.37 +                       | $(BIN)/FOL;\
   26.38 +                fi;;\
   26.39  	*)	echo Bad value for ISABELLECOMP: \
   26.40                  	$(COMP) is not poly or sml; exit 1;;\
   26.41  	esac
    27.1 --- a/src/ZF/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    27.2 +++ b/src/ZF/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    27.3 @@ -40,4 +40,6 @@
    27.4  (*printing functions are inherited from FOL*)
    27.5  print_depth 8;
    27.6  
    27.7 +make_chart ();   (*make HTML chart*)
    27.8 +
    27.9  val ZF_build_completed = ();	(*indicate successful build*)
    28.1 --- a/src/ZF/Resid/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    28.2 +++ b/src/ZF/Resid/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    28.3 @@ -21,4 +21,6 @@
    28.4  
    28.5  time_use_thy "Confluence";
    28.6  
    28.7 +make_chart ();   (*make HTML chart*)
    28.8 +
    28.9  writeln"END: Root file for ZF/Resid";
    29.1 --- a/src/ZF/ex/ROOT.ML	Tue Oct 24 14:49:45 1995 +0100
    29.2 +++ b/src/ZF/ex/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
    29.3 @@ -42,4 +42,6 @@
    29.4  time_use_thy "ex/LList";
    29.5  time_use_thy "ex/CoUnit";
    29.6  
    29.7 +make_chart ();   (*make HTML chart*)
    29.8 +
    29.9  writeln"END: Root file for ZF Set Theory examples";