Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
main directory is now read by exit_use_dir, too;
authorclasohm
Tue, 21 Nov 1995 15:10:12 +0100
changeset 1361 90d615b599d9
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 file | annotate | diff | comparison | revisions
src/CCL/ROOT.ML file | annotate | diff | comparison | revisions
src/CTT/Makefile file | annotate | diff | comparison | revisions
src/CTT/ROOT.ML file | annotate | diff | comparison | revisions
src/Cube/Makefile file | annotate | diff | comparison | revisions
src/Cube/ROOT.ML file | annotate | diff | comparison | revisions
src/FOLP/Makefile file | annotate | diff | comparison | revisions
src/FOLP/ROOT.ML file | annotate | diff | comparison | revisions
src/HOLCF/Makefile file | annotate | diff | comparison | revisions
src/HOLCF/ROOT.ML file | annotate | diff | comparison | revisions
src/LCF/Makefile file | annotate | diff | comparison | revisions
src/LCF/ROOT.ML file | annotate | diff | comparison | revisions
src/LK/Makefile file | annotate | diff | comparison | revisions
src/LK/ROOT.ML file | annotate | diff | comparison | revisions
src/Modal/Makefile file | annotate | diff | comparison | revisions
src/Modal/ROOT.ML file | annotate | diff | comparison | revisions
src/ZF/Makefile file | annotate | diff | comparison | revisions
src/ZF/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/CCL/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CCL/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -37,13 +37,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CCL;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CCL;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(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;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/CCL/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CCL/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val CCL_build_completed = ();   (*indicate successful build*)
--- a/src/CTT/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CTT/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -36,13 +36,14 @@
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/CTT;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/CTT;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/CTT/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/CTT/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -23,6 +23,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val CTT_build_completed = ();	(*indicate successful build*)
--- a/src/Cube/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Cube/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,14 +29,14 @@
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Cube;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Cube;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/Cube/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Cube/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -17,6 +17,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val Cube_build_completed = ();	(*indicate successful build*)
--- a/src/FOLP/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/FOLP/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -33,14 +33,14 @@
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/FOLP;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/FOLP;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/FOLP" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/FOLP/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/FOLP/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -78,6 +78,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val FOLP_build_completed = ();	(*indicate successful build*)
--- a/src/HOLCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/HOLCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -37,14 +37,14 @@
 	case "$(COMP)" in \
 	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/HOLCF;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/HOLCF;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
                        | $(BIN)/HOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/HOLCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/HOLCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 
 print_depth 100;  
 
-make_chart ();   (*make HTML chart*)
-
 val HOLCF_build_completed = ();	(*indicate successful build*)
--- a/src/LCF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LCF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -28,13 +28,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LCF;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LCF;\
+		else echo 'open PolyML; exit_use_dir".";' \
+                       | $(COMP) $(BIN)/LCF;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LCF" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/LCF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LCF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -17,6 +17,4 @@
 use"pair.ML";
 use"fix.ML";
 
-make_chart ();   (*make HTML chart*)
-
 val LCF_build_completed = ();	(*indicate successful build*)
--- a/src/LK/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LK/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,13 +29,13 @@
 	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/LK;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK;\
+		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/LK;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/LK" banner;' \
                        | $(BIN)/Pure;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/LK/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/LK/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -19,6 +19,4 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val LK_build_completed = ();	(*indicate successful build*)
--- a/src/Modal/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Modal/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -29,14 +29,14 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/LK $(BIN)/Modal;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/Modal;\
-		else echo 'open PolyML; exit_use"ROOT";' \
+		else echo 'open PolyML; exit_use_dir".";' \
 		       | $(COMP) $(BIN)/Modal;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Modal" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
                        | $(BIN)/LK;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/Modal/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/Modal/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -78,8 +78,6 @@
 end;
 structure S43_Prover = Modal_ProverFun(MP_Rule);  
 
-make_chart ();   (*make HTML chart*)
-
 val Modal_build_completed = ();	(*indicate successful build*)
 
 (*printing functions are inherited from LK*)
--- a/src/ZF/Makefile	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/ZF/Makefile	Tue Nov 21 15:10:12 1995 +0100
@@ -38,13 +38,13 @@
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
                 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
                        | $(COMP) $(BIN)/ZF;\
-		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF;\
+		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/ZF;\
                 fi;;\
 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
-                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' \
+                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
+                else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
                        | $(BIN)/FOL;\
                 fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/ZF/ROOT.ML	Tue Nov 21 14:53:03 1995 +0100
+++ b/src/ZF/ROOT.ML	Tue Nov 21 15:10:12 1995 +0100
@@ -40,6 +40,4 @@
 (*printing functions are inherited from FOL*)
 print_depth 8;
 
-make_chart ();   (*make HTML chart*)
-
 val ZF_build_completed = ();	(*indicate successful build*)
isabelle