main directory is now read by exit_use_dir, too;
authorclasohm
Tue Nov 21 15:10:12 1995 +0100 (1995-11-21)
changeset 136190d615b599d9
parent 1360 6bdee79ef125
child 1362 5fdd4da11d49
main directory is now read by exit_use_dir, too;
removed make_chart from ROOT.ML
src/CCL/Makefile
src/CCL/ROOT.ML
src/CTT/Makefile
src/CTT/ROOT.ML
src/Cube/Makefile
src/Cube/ROOT.ML
src/FOLP/Makefile
src/FOLP/ROOT.ML
src/HOLCF/Makefile
src/HOLCF/ROOT.ML
src/LCF/Makefile
src/LCF/ROOT.ML
src/LK/Makefile
src/LK/ROOT.ML
src/Modal/Makefile
src/Modal/ROOT.ML
src/ZF/Makefile
src/ZF/ROOT.ML
     1.1 --- a/src/CCL/Makefile	Tue Nov 21 14:53:03 1995 +0100
     1.2 +++ b/src/CCL/Makefile	Tue Nov 21 15:10:12 1995 +0100
     1.3 @@ -37,13 +37,14 @@
     1.4  	case "$(COMP)" in \
     1.5  	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
     1.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     1.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
     1.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
     1.9                         | $(COMP) $(BIN)/CCL;\
    1.10 -		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CCL;\
    1.11 +		else echo 'open PolyML; exit_use_dir".";' \
    1.12 +                       | $(COMP) $(BIN)/CCL;\
    1.13                  fi;;\
    1.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CCL" banner;' \
    1.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
    1.19                         | $(BIN)/FOL;\
    1.20                  fi;;\
    1.21  	*)	echo Bad value for ISABELLECOMP: \
     2.1 --- a/src/CCL/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
     2.2 +++ b/src/CCL/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
     2.3 @@ -40,6 +40,4 @@
     2.4  
     2.5  print_depth 8;
     2.6  
     2.7 -make_chart ();   (*make HTML chart*)
     2.8 -
     2.9  val CCL_build_completed = ();   (*indicate successful build*)
     3.1 --- a/src/CTT/Makefile	Tue Nov 21 14:53:03 1995 +0100
     3.2 +++ b/src/CTT/Makefile	Tue Nov 21 15:10:12 1995 +0100
     3.3 @@ -36,13 +36,14 @@
     3.4  	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
     3.5  			| $(COMP) $(BIN)/Pure;\
     3.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     3.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
     3.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
     3.9                         | $(COMP) $(BIN)/CTT;\
    3.10 -		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT;\
    3.11 +		else echo 'open PolyML; exit_use_dir".";' \
    3.12 +                       | $(COMP) $(BIN)/CTT;\
    3.13                  fi;;\
    3.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    3.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' \
    3.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    3.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
    3.19                         | $(BIN)/Pure;\
    3.20                  fi;;\
    3.21  	*)	echo Bad value for ISABELLECOMP: \
     4.1 --- a/src/CTT/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
     4.2 +++ b/src/CTT/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
     4.3 @@ -23,6 +23,4 @@
     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 CTT_build_completed = ();	(*indicate successful build*)
     5.1 --- a/src/Cube/Makefile	Tue Nov 21 14:53:03 1995 +0100
     5.2 +++ b/src/Cube/Makefile	Tue Nov 21 15:10:12 1995 +0100
     5.3 @@ -29,14 +29,14 @@
     5.4  	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
     5.5  			| $(COMP) $(BIN)/Pure;\
     5.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     5.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
     5.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
     5.9                         | $(COMP) $(BIN)/Cube;\
    5.10 -		else echo 'open PolyML; exit_use"ROOT";' \
    5.11 +		else echo 'open PolyML; exit_use_dir".";' \
    5.12  		       | $(COMP) $(BIN)/Cube;\
    5.13                  fi;;\
    5.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    5.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' \
    5.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    5.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
    5.19                         | $(BIN)/Pure;\
    5.20                  fi;;\
    5.21  	*)	echo Bad value for ISABELLECOMP: \
     6.1 --- a/src/Cube/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
     6.2 +++ b/src/Cube/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
     6.3 @@ -17,6 +17,4 @@
     6.4  use "../Pure/install_pp.ML";
     6.5  print_depth 8;
     6.6  
     6.7 -make_chart ();   (*make HTML chart*)
     6.8 -
     6.9  val Cube_build_completed = ();	(*indicate successful build*)
     7.1 --- a/src/FOLP/Makefile	Tue Nov 21 14:53:03 1995 +0100
     7.2 +++ b/src/FOLP/Makefile	Tue Nov 21 15:10:12 1995 +0100
     7.3 @@ -33,14 +33,14 @@
     7.4  	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
     7.5  			| $(COMP) $(BIN)/Pure;\
     7.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     7.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
     7.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
     7.9                         | $(COMP) $(BIN)/FOLP;\
    7.10 -		else echo 'open PolyML; exit_use"ROOT";' \
    7.11 +		else echo 'open PolyML; exit_use_dir".";' \
    7.12  		       | $(COMP) $(BIN)/FOLP;\
    7.13                  fi;;\
    7.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    7.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    7.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' \
    7.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    7.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    7.19                         | $(BIN)/Pure;\
    7.20                  fi;;\
    7.21  	*)	echo Bad value for ISABELLECOMP: \
     8.1 --- a/src/FOLP/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
     8.2 +++ b/src/FOLP/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
     8.3 @@ -78,6 +78,4 @@
     8.4  use "../Pure/install_pp.ML";
     8.5  print_depth 8;
     8.6  
     8.7 -make_chart ();   (*make HTML chart*)
     8.8 -
     8.9  val FOLP_build_completed = ();	(*indicate successful build*)
     9.1 --- a/src/HOLCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
     9.2 +++ b/src/HOLCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
     9.3 @@ -37,14 +37,14 @@
     9.4  	case "$(COMP)" in \
     9.5  	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
     9.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
     9.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
     9.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
     9.9                         | $(COMP) $(BIN)/HOLCF;\
    9.10 -		else echo 'open PolyML; exit_use"ROOT";' \
    9.11 +		else echo 'open PolyML; exit_use_dir".";' \
    9.12  		       | $(COMP) $(BIN)/HOLCF;\
    9.13                  fi;;\
    9.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    9.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    9.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' \
    9.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    9.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
    9.19                         | $(BIN)/HOL;\
    9.20                  fi;;\
    9.21  	*)	echo Bad value for ISABELLECOMP: \
    10.1 --- a/src/HOLCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
    10.2 +++ b/src/HOLCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
    10.3 @@ -40,6 +40,4 @@
    10.4  
    10.5  print_depth 100;  
    10.6  
    10.7 -make_chart ();   (*make HTML chart*)
    10.8 -
    10.9  val HOLCF_build_completed = ();	(*indicate successful build*)
    11.1 --- a/src/LCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
    11.2 +++ b/src/LCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
    11.3 @@ -28,13 +28,14 @@
    11.4  	case "$(COMP)" in \
    11.5  	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
    11.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    11.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    11.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    11.9                         | $(COMP) $(BIN)/LCF;\
   11.10 -		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF;\
   11.11 +		else echo 'open PolyML; exit_use_dir".";' \
   11.12 +                       | $(COMP) $(BIN)/LCF;\
   11.13                  fi;;\
   11.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   11.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
   11.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' \
   11.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
   11.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
   11.19                         | $(BIN)/FOL;\
   11.20                  fi;;\
   11.21  	*)	echo Bad value for ISABELLECOMP: \
    12.1 --- a/src/LCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
    12.2 +++ b/src/LCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
    12.3 @@ -17,6 +17,4 @@
    12.4  use"pair.ML";
    12.5  use"fix.ML";
    12.6  
    12.7 -make_chart ();   (*make HTML chart*)
    12.8 -
    12.9  val LCF_build_completed = ();	(*indicate successful build*)
    13.1 --- a/src/LK/Makefile	Tue Nov 21 14:53:03 1995 +0100
    13.2 +++ b/src/LK/Makefile	Tue Nov 21 15:10:12 1995 +0100
    13.3 @@ -29,13 +29,13 @@
    13.4  	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
    13.5  			| $(COMP) $(BIN)/Pure;\
    13.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    13.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    13.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    13.9                         | $(COMP) $(BIN)/LK;\
   13.10 -		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK;\
   13.11 +		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
   13.12                  fi;;\
   13.13  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   13.14 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
   13.15 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' \
   13.16 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
   13.17 +                else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
   13.18                         | $(BIN)/Pure;\
   13.19                  fi;;\
   13.20  	*)	echo Bad value for ISABELLECOMP: \
    14.1 --- a/src/LK/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
    14.2 +++ b/src/LK/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
    14.3 @@ -19,6 +19,4 @@
    14.4  use "../Pure/install_pp.ML";
    14.5  print_depth 8;
    14.6  
    14.7 -make_chart ();   (*make HTML chart*)
    14.8 -
    14.9  val LK_build_completed = ();	(*indicate successful build*)
    15.1 --- a/src/Modal/Makefile	Tue Nov 21 14:53:03 1995 +0100
    15.2 +++ b/src/Modal/Makefile	Tue Nov 21 15:10:12 1995 +0100
    15.3 @@ -29,14 +29,14 @@
    15.4  	case "$(COMP)" in \
    15.5  	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
    15.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    15.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    15.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    15.9                         | $(COMP) $(BIN)/Modal;\
   15.10 -		else echo 'open PolyML; exit_use"ROOT";' \
   15.11 +		else echo 'open PolyML; exit_use_dir".";' \
   15.12  		       | $(COMP) $(BIN)/Modal;\
   15.13                  fi;;\
   15.14  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   15.15 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
   15.16 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' \
   15.17 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
   15.18 +                else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
   15.19                         | $(BIN)/LK;\
   15.20                  fi;;\
   15.21  	*)	echo Bad value for ISABELLECOMP: \
    16.1 --- a/src/Modal/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
    16.2 +++ b/src/Modal/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
    16.3 @@ -78,8 +78,6 @@
    16.4  end;
    16.5  structure S43_Prover = Modal_ProverFun(MP_Rule);  
    16.6  
    16.7 -make_chart ();   (*make HTML chart*)
    16.8 -
    16.9  val Modal_build_completed = ();	(*indicate successful build*)
   16.10  
   16.11  (*printing functions are inherited from LK*)
    17.1 --- a/src/ZF/Makefile	Tue Nov 21 14:53:03 1995 +0100
    17.2 +++ b/src/ZF/Makefile	Tue Nov 21 15:10:12 1995 +0100
    17.3 @@ -38,13 +38,13 @@
    17.4  	case "$(COMP)" in \
    17.5  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
    17.6                  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    17.7 -                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    17.8 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    17.9                         | $(COMP) $(BIN)/ZF;\
   17.10 -		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\
   17.11 +		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/ZF;\
   17.12                  fi;;\
   17.13  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   17.14 -                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   17.15 -                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' \
   17.16 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   17.17 +                else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
   17.18                         | $(BIN)/FOL;\
   17.19                  fi;;\
   17.20  	*)	echo Bad value for ISABELLECOMP: \
    18.1 --- a/src/ZF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
    18.2 +++ b/src/ZF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
    18.3 @@ -40,6 +40,4 @@
    18.4  (*printing functions are inherited from FOL*)
    18.5  print_depth 8;
    18.6  
    18.7 -make_chart ();   (*make HTML chart*)
    18.8 -
    18.9  val ZF_build_completed = ();	(*indicate successful build*)