# HG changeset patch # User clasohm # Date 814542135 -3600 # Node ID 4ade5d1d369c7c6c4a1ce66ddc5b4a7550a8d871 # Parent f5547274504472a647842265253b68c3351782ed added calls of init_html and make_chart diff -r f55472745044 -r 4ade5d1d369c src/CCL/Makefile --- a/src/CCL/Makefile Tue Oct 24 13:54:00 1995 +0100 +++ b/src/CCL/Makefile Tue Oct 24 14:42:15 1995 +0100 @@ -1,4 +1,4 @@ -# $Id$ +# $Id$ ######################################################################### # # # Makefile for Isabelle (CCL) # @@ -6,9 +6,11 @@ ######################################################################### #To make the system, cd to this directory and type -# make -f Makefile +# make #To make the system and test it on standard examples, type -# make -f Makefile test +# make test +#To generate HTML files for every theory, set the environment variable +#MAKE_HTML or add the parameter "MAKE_HTML=". #Environment variable ISABELLECOMP specifies the compiler. #Environment variable ISABELLEBIN specifies the destination directory. @@ -34,8 +36,16 @@ $(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES) case "$(COMP)" in \ poly*) cp $(BIN)/FOL $(BIN)/CCL;\ - echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CCL ;;\ - sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;;\ + if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ + then echo 'open PolyML; init_html (); exit_use"ROOT";' \ + | $(COMP) $(BIN)/CCL;\ + else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CCL;\ + fi;;\ + sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ + then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\ + else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CCL" banner;' \ + | $(BIN)/FOL;\ + fi;;\ *) echo Bad value for ISABELLECOMP: \ $(COMP) is not poly or sml;;\ esac diff -r f55472745044 -r 4ade5d1d369c src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Tue Oct 24 13:54:00 1995 +0100 +++ b/src/CCL/ROOT.ML Tue Oct 24 14:42:15 1995 +0100 @@ -40,4 +40,6 @@ print_depth 8; +make_chart (); (*make HTML chart*) + val CCL_build_completed = (); (*indicate successful build*) diff -r f55472745044 -r 4ade5d1d369c src/CCL/ex/ROOT.ML --- a/src/CCL/ex/ROOT.ML Tue Oct 24 13:54:00 1995 +0100 +++ b/src/CCL/ex/ROOT.ML Tue Oct 24 14:42:15 1995 +0100 @@ -16,4 +16,7 @@ time_use_thy "ex/List"; time_use_thy "ex/Stream"; time_use_thy "ex/Flag"; + +make_chart (); (*make HTML chart*) + maketest"END: Root file for CCL examples";