# HG changeset patch
# User clasohm
# Date 814543157 -3600
# Node ID f04b33ce250f77c9a18c59f73fb71921cf54995e
# Parent  093e273405f04f30f5a265553fa9cd5d94b69bf2
added calls of init_html and make_chart

diff -r 093e273405f0 -r f04b33ce250f IMP/ROOT.ML
--- a/IMP/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/IMP/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -19,3 +19,6 @@
 loadpath := [".","IMP"];
 time_use_thy "Properties";
 time_use_thy "Equiv";
+
+make_chart ();   (*make HTML chart*)
+
diff -r 093e273405f0 -r f04b33ce250f IOA/ROOT.ML
--- a/IOA/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/IOA/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -20,3 +20,5 @@
 
 loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
 use_thy "Correctness";
+
+make_chart ();   (*make HTML chart*)
diff -r 093e273405f0 -r f04b33ce250f Integ/ROOT.ML
--- a/Integ/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/Integ/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:  	HOL/Integ/ROOT
+(*  Title:  	Old_HOL/Integ/ROOT.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -10,3 +10,5 @@
 
 loadpath := ["Integ"];
 time_use_thy "Integ";
+
+make_chart ();   (*make HTML chart*)
diff -r 093e273405f0 -r f04b33ce250f Makefile
--- a/Makefile	Thu Jun 29 12:29:58 1995 +0200
+++ b/Makefile	Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-#  $Id$
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (Old_HOL)			#
@@ -6,9 +6,9 @@
 #########################################################################
 
 #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
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -38,9 +38,17 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/Old_HOL"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Old_HOL;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | \
-                     $(BIN)/Pure ;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/Old_HOL;\
+		else echo 'open PolyML; exit_use"ROOT";' \
+		       | $(COMP) $(BIN)/Old_HOL;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/Old_HOL" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml; exit 1;;\
 	esac
diff -r 093e273405f0 -r f04b33ce250f ROOT.ML
--- a/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -1,10 +1,10 @@
-(*  Title:      HOL/ROOT.ML
+(*  Title:      Old_HOL/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
 Adds Classical Higher-order Logic to a database containing Pure Isabelle.
-Should be executed in the subdirectory HOL.
+Should be executed in the subdirectory Old_HOL.
 *)
 
 val banner = "Higher-Order Logic";
@@ -18,7 +18,6 @@
 use "thy_syntax.ML";
 
 use_thy "HOL";
-use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
@@ -86,4 +85,6 @@
 init_pps ();
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val HOL_build_completed = ();   (*indicate successful build*)
diff -r 093e273405f0 -r f04b33ce250f Subst/ROOT.ML
--- a/Subst/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/Subst/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/Subst
+(*  Title: 	Old_HOL/Subst/ROOT.ML
     Author: 	Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -35,3 +35,5 @@
 use_thy "Subst/Subst";
 use_thy "Subst/Unifier";
 writeln"END: Root file for Substitutions and Unification";
+
+make_chart ();   (*make HTML chart*)
diff -r 093e273405f0 -r f04b33ce250f ex/ROOT.ML
--- a/ex/ROOT.ML	Thu Jun 29 12:29:58 1995 +0200
+++ b/ex/ROOT.ML	Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:  	HOL/ex/ROOT
+(*  Title:  	Old_HOL/ex/ROOT.ML
     ID:         $Id$
     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -28,4 +28,7 @@
 time_use_thy "Term";
 time_use_thy "Simult";
 time_use_thy "MT";
+
+make_chart ();   (*make HTML chart*)
+
 writeln     "END: Root file for HOL examples";