# HG changeset patch
# User wenzelm
# Date 862925255 -7200
# Node ID 24dae6222579ad9457d39599bd7ebf0f88e6ca28
# Parent  74c1b51c1cd930468ace1d1ec3caa0bc8122d2ef
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);

diff -r 74c1b51c1cd9 -r 24dae6222579 bin/isabelle
--- a/bin/isabelle	Tue May 06 15:24:41 1997 +0200
+++ b/bin/isabelle	Tue May 06 15:27:35 1997 +0200
@@ -148,8 +148,8 @@
     OUTFILE="$OUTPUT"
     ;;
   *)
-    mkdir -p "$ISABELLE_OUTPUT_DIR"
-    OUTFILE="$ISABELLE_OUTPUT_DIR/$OUTPUT"
+    mkdir -p "$ISABELLE_OUTPUT"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
     ;;
 esac
 
diff -r 74c1b51c1cd9 -r 24dae6222579 etc/settings
--- a/etc/settings	Tue May 06 15:24:41 1997 +0200
+++ b/etc/settings	Tue May 06 15:27:35 1997 +0200
@@ -56,16 +56,17 @@
 ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools
 
 
-# Heap file locations.
+# Heap file locations. ML system identifier appended automatically!
 
-ISABELLE_PATH=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM:$ISABELLE_HOME/heaps/$ML_SYSTEM
+ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
 
 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
-  ISABELLE_OUTPUT_DIR=$ISABELLE_HOME/heaps/$ML_SYSTEM
+  ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
 else
-  ISABELLE_OUTPUT_DIR=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM
+  ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps
 fi
 
+
 DEFAULT_LOGIC=HOL
 
 
diff -r 74c1b51c1cd9 -r 24dae6222579 etc/user-settings.sample
--- a/etc/user-settings.sample	Tue May 06 15:24:41 1997 +0200
+++ b/etc/user-settings.sample	Tue May 06 15:27:35 1997 +0200
@@ -15,7 +15,10 @@
 ### Heap files
 ###
 
+# Note: ML system identifier appended automatically!
+
 #ISABELLE_PATH=other-places-where-heaps-may-reside:$ISABELLE_PATH
+#ISABELLE_OUTPUT=somewhere-else
 
 #DEFAULT_LOGIC=ZF
 
diff -r 74c1b51c1cd9 -r 24dae6222579 lib/Tools/makeall
--- a/lib/Tools/makeall	Tue May 06 15:24:41 1997 +0200
+++ b/lib/Tools/makeall	Tue May 06 15:27:35 1997 +0200
@@ -47,7 +47,7 @@
 
 echo Started at `date`
 echo Source=`pwd`
-echo Destination=$ISABELLE_OUTPUT_DIR
+echo Destination=$ISABELLE_OUTPUT
 echo force=$FORCE '    ' clean=$CLEAN '    '
 echo Compiler=$ML_SYSTEM
 echo Running on `hostname`
@@ -57,10 +57,10 @@
         echo '		**** Consider the -notest switch ****'
 esac
 
-mkdir -p $ISABELLE_OUTPUT_DIR
+mkdir -p $ISABELLE_OUTPUT
 
 case $FORCE.$EXEC in
-  on.on) (cd $ISABELLE_OUTPUT_DIR;
+  on.on) (cd $ISABELLE_OUTPUT;
           for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
 	  do 
 	   rm -f $f
@@ -91,7 +91,7 @@
 tail ZF/make$$.log
 gzip ZF/make$$.log
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/ZF
+    on.on)	rm -f $ISABELLE_OUTPUT/ZF
 esac
 
 echo
@@ -101,7 +101,7 @@
 tail CCL/make$$.log
 gzip CCL/make$$.log
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CCL
+    on.on)	rm -f $ISABELLE_OUTPUT/CCL
 esac
 
 echo
@@ -111,7 +111,7 @@
 tail LCF/make$$.log
 gzip LCF/make$$.log
 case $CLEAN.$EXEC in
-  on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF
+  on.on)	rm -f $ISABELLE_OUTPUT/FOL $ISABELLE_OUTPUT/LCF
 esac
 
 echo
@@ -121,7 +121,7 @@
 tail CTT/make$$.log
 gzip CTT/make$$.log
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CTT
+    on.on)	rm -f $ISABELLE_OUTPUT/CTT
 esac
 
 echo
@@ -131,7 +131,7 @@
 tail Sequents/make$$.log
 gzip Sequents/make$$.log
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Sequents
+    on.on)	rm -f $ISABELLE_OUTPUT/Sequents
 esac
 
 echo
@@ -149,7 +149,7 @@
 tail HOLCF/make$$.log
 gzip HOLCF/make$$.log
 case $CLEAN.$EXEC in
-  on.on)	rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF
+  on.on)	rm -f $ISABELLE_OUTPUT/HOL $ISABELLE_OUTPUT/HOLCF
 esac
 
 echo
@@ -157,7 +157,7 @@
 echo '*****The Lambda-Cube (Cube)*****'
 (cd Cube; $ISATOOL make $NO $TEST > make$$.log)
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Cube
+    on.on)	rm -f $ISABELLE_OUTPUT/Cube
 esac
 tail Cube/make$$.log 
 gzip Cube/make$$.log 
@@ -167,7 +167,7 @@
 echo '*****First-Order Logic with Proof Terms (FOLP)*****'
 (cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
 case $CLEAN.$EXEC in
-    on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOLP
+    on.on)	rm -f $ISABELLE_OUTPUT/FOLP
 esac
 tail FOLP/make$$.log 
 gzip FOLP/make$$.log 
diff -r 74c1b51c1cd9 -r 24dae6222579 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue May 06 15:24:41 1997 +0200
+++ b/lib/scripts/getsettings	Tue May 06 15:27:35 1997 +0200
@@ -23,4 +23,9 @@
 ISABELLE=$ISABELLE_HOME/bin/isabelle
 ISATOOL=$ISABELLE_HOME/bin/isatool
 
+#append ML system to paths
+ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
+ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
+ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
+
 set +o allexport
diff -r 74c1b51c1cd9 -r 24dae6222579 src/CCL/IsaMakefile
--- a/src/CCL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/CCL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for CCL
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
 	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
diff -r 74c1b51c1cd9 -r 24dae6222579 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/CTT/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for CTT
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 FILES =	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
 	Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
diff -r 74c1b51c1cd9 -r 24dae6222579 src/Cube/IsaMakefile
--- a/src/Cube/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/Cube/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for Cube
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 FILES =	ROOT.ML Cube.thy Cube.ML
 
 $(OUT)/Cube: $(OUT)/Pure $(FILES)
diff -r 74c1b51c1cd9 -r 24dae6222579 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/FOL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for FOL
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
 	thy_data.ML cladata.ML \
diff -r 74c1b51c1cd9 -r 24dae6222579 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/FOLP/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for FOLP
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 FILES =	ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
 	hypsubst.ML classical.ML simp.ML
diff -r 74c1b51c1cd9 -r 24dae6222579 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/HOL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
 
 #### Base system
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
diff -r 74c1b51c1cd9 -r 24dae6222579 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/HOLCF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
 
 #### Base system
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 THYS = Porder.thy Porder0.thy Pcpo.thy \
        Fun1.thy Fun2.thy Fun3.thy \
diff -r 74c1b51c1cd9 -r 24dae6222579 src/LCF/IsaMakefile
--- a/src/LCF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/LCF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for LCF
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 FILES =	ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
 
 $(OUT)/LCF: $(OUT)/FOL $(FILES)
diff -r 74c1b51c1cd9 -r 24dae6222579 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/Pure/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -7,7 +7,7 @@
 # are loaded on top of it.
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
 	ML-Systems/smlnj-1.07.ML ML-Systems/smlnj-1.09.ML ROOT.ML \
diff -r 74c1b51c1cd9 -r 24dae6222579 src/Pure/mk
--- a/src/Pure/mk	Tue May 06 15:24:41 1997 +0200
+++ b/src/Pure/mk	Tue May 06 15:27:35 1997 +0200
@@ -32,4 +32,4 @@
   -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
   -q RAW_ML_SYSTEM Pure
 
-chmod -w $ISABELLE_OUTPUT_DIR/Pure
+chmod -w $ISABELLE_OUTPUT/Pure
diff -r 74c1b51c1cd9 -r 24dae6222579 src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/Sequents/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -4,7 +4,7 @@
 # IsaMakefile for Sequents
 #
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 NAMES = ILL LK S4 S43 T
 FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
diff -r 74c1b51c1cd9 -r 24dae6222579 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
+++ b/src/ZF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
@@ -6,7 +6,7 @@
 
 #### Base system
 
-OUT = $(ISABELLE_OUTPUT_DIR)
+OUT = $(ISABELLE_OUTPUT)
 
 NAMES = ZF upair subset pair domrange \
 	func AC equalities Bool \