1.1 --- a/bin/isabelle	Tue May 06 15:24:41 1997 +0200
     1.2 +++ b/bin/isabelle	Tue May 06 15:27:35 1997 +0200
     1.3 @@ -148,8 +148,8 @@
     1.4      OUTFILE="$OUTPUT"
     1.5      ;;
     1.6    *)
     1.7 -    mkdir -p "$ISABELLE_OUTPUT_DIR"
     1.8 -    OUTFILE="$ISABELLE_OUTPUT_DIR/$OUTPUT"
     1.9 +    mkdir -p "$ISABELLE_OUTPUT"
    1.10 +    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
    1.11      ;;
    1.12  esac
    1.13  

     2.1 --- a/etc/settings	Tue May 06 15:24:41 1997 +0200
     2.2 +++ b/etc/settings	Tue May 06 15:27:35 1997 +0200
     2.3 @@ -56,16 +56,17 @@
     2.4  ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools
     2.5  
     2.6  
     2.7 -# Heap file locations.
     2.8 +# Heap file locations. ML system identifier appended automatically!
     2.9  
    2.10 -ISABELLE_PATH=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM:$ISABELLE_HOME/heaps/$ML_SYSTEM
    2.11 +ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
    2.12  
    2.13  if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    2.14 -  ISABELLE_OUTPUT_DIR=$ISABELLE_HOME/heaps/$ML_SYSTEM
    2.15 +  ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
    2.16  else
    2.17 -  ISABELLE_OUTPUT_DIR=$ISABELLE_HOME_USER/heaps/$ML_SYSTEM
    2.18 +  ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps
    2.19  fi
    2.20  
    2.21 +
    2.22  DEFAULT_LOGIC=HOL
    2.23  
    2.24  

     3.1 --- a/etc/user-settings.sample	Tue May 06 15:24:41 1997 +0200
     3.2 +++ b/etc/user-settings.sample	Tue May 06 15:27:35 1997 +0200
     3.3 @@ -15,7 +15,10 @@
     3.4  ### Heap files
     3.5  ###
     3.6  
     3.7 +# Note: ML system identifier appended automatically!
     3.8 +
     3.9  #ISABELLE_PATH=other-places-where-heaps-may-reside:$ISABELLE_PATH
    3.10 +#ISABELLE_OUTPUT=somewhere-else
    3.11  
    3.12  #DEFAULT_LOGIC=ZF
    3.13  

     4.1 --- a/lib/Tools/makeall	Tue May 06 15:24:41 1997 +0200
     4.2 +++ b/lib/Tools/makeall	Tue May 06 15:27:35 1997 +0200
     4.3 @@ -47,7 +47,7 @@
     4.4  
     4.5  echo Started at `date`
     4.6  echo Source=`pwd`
     4.7 -echo Destination=$ISABELLE_OUTPUT_DIR
     4.8 +echo Destination=$ISABELLE_OUTPUT
     4.9  echo force=$FORCE '    ' clean=$CLEAN '    '
    4.10  echo Compiler=$ML_SYSTEM
    4.11  echo Running on `hostname`
    4.12 @@ -57,10 +57,10 @@
    4.13          echo '		**** Consider the -notest switch ****'
    4.14  esac
    4.15  
    4.16 -mkdir -p $ISABELLE_OUTPUT_DIR
    4.17 +mkdir -p $ISABELLE_OUTPUT
    4.18  
    4.19  case $FORCE.$EXEC in
    4.20 -  on.on) (cd $ISABELLE_OUTPUT_DIR;
    4.21 +  on.on) (cd $ISABELLE_OUTPUT;
    4.22            for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
    4.23  	  do 
    4.24  	   rm -f $f
    4.25 @@ -91,7 +91,7 @@
    4.26  tail ZF/make$$.log
    4.27  gzip ZF/make$$.log
    4.28  case $CLEAN.$EXEC in
    4.29 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/ZF
    4.30 +    on.on)	rm -f $ISABELLE_OUTPUT/ZF
    4.31  esac
    4.32  
    4.33  echo
    4.34 @@ -101,7 +101,7 @@
    4.35  tail CCL/make$$.log
    4.36  gzip CCL/make$$.log
    4.37  case $CLEAN.$EXEC in
    4.38 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CCL
    4.39 +    on.on)	rm -f $ISABELLE_OUTPUT/CCL
    4.40  esac
    4.41  
    4.42  echo
    4.43 @@ -111,7 +111,7 @@
    4.44  tail LCF/make$$.log
    4.45  gzip LCF/make$$.log
    4.46  case $CLEAN.$EXEC in
    4.47 -  on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF
    4.48 +  on.on)	rm -f $ISABELLE_OUTPUT/FOL $ISABELLE_OUTPUT/LCF
    4.49  esac
    4.50  
    4.51  echo
    4.52 @@ -121,7 +121,7 @@
    4.53  tail CTT/make$$.log
    4.54  gzip CTT/make$$.log
    4.55  case $CLEAN.$EXEC in
    4.56 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CTT
    4.57 +    on.on)	rm -f $ISABELLE_OUTPUT/CTT
    4.58  esac
    4.59  
    4.60  echo
    4.61 @@ -131,7 +131,7 @@
    4.62  tail Sequents/make$$.log
    4.63  gzip Sequents/make$$.log
    4.64  case $CLEAN.$EXEC in
    4.65 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Sequents
    4.66 +    on.on)	rm -f $ISABELLE_OUTPUT/Sequents
    4.67  esac
    4.68  
    4.69  echo
    4.70 @@ -149,7 +149,7 @@
    4.71  tail HOLCF/make$$.log
    4.72  gzip HOLCF/make$$.log
    4.73  case $CLEAN.$EXEC in
    4.74 -  on.on)	rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF
    4.75 +  on.on)	rm -f $ISABELLE_OUTPUT/HOL $ISABELLE_OUTPUT/HOLCF
    4.76  esac
    4.77  
    4.78  echo
    4.79 @@ -157,7 +157,7 @@
    4.80  echo '*****The Lambda-Cube (Cube)*****'
    4.81  (cd Cube; $ISATOOL make $NO $TEST > make$$.log)
    4.82  case $CLEAN.$EXEC in
    4.83 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Cube
    4.84 +    on.on)	rm -f $ISABELLE_OUTPUT/Cube
    4.85  esac
    4.86  tail Cube/make$$.log 
    4.87  gzip Cube/make$$.log 
    4.88 @@ -167,7 +167,7 @@
    4.89  echo '*****First-Order Logic with Proof Terms (FOLP)*****'
    4.90  (cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
    4.91  case $CLEAN.$EXEC in
    4.92 -    on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOLP
    4.93 +    on.on)	rm -f $ISABELLE_OUTPUT/FOLP
    4.94  esac
    4.95  tail FOLP/make$$.log 
    4.96  gzip FOLP/make$$.log 

     5.1 --- a/lib/scripts/getsettings	Tue May 06 15:24:41 1997 +0200
     5.2 +++ b/lib/scripts/getsettings	Tue May 06 15:27:35 1997 +0200
     5.3 @@ -23,4 +23,9 @@
     5.4  ISABELLE=$ISABELLE_HOME/bin/isabelle
     5.5  ISATOOL=$ISABELLE_HOME/bin/isatool
     5.6  
     5.7 +#append ML system to paths
     5.8 +ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM"
     5.9 +ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done)
    5.10 +ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
    5.11 +
    5.12  set +o allexport

     6.1 --- a/src/CCL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
     6.2 +++ b/src/CCL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  # IsaMakefile for CCL
     6.5  #
     6.6  
     6.7 -OUT = $(ISABELLE_OUTPUT_DIR)
     6.8 +OUT = $(ISABELLE_OUTPUT)
     6.9  
    6.10  SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
    6.11  	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML

     7.1 --- a/src/CTT/IsaMakefile	Tue May 06 15:24:41 1997 +0200
     7.2 +++ b/src/CTT/IsaMakefile	Tue May 06 15:27:35 1997 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  # IsaMakefile for CTT
     7.5  #
     7.6  
     7.7 -OUT = $(ISABELLE_OUTPUT_DIR)
     7.8 +OUT = $(ISABELLE_OUTPUT)
     7.9  
    7.10  FILES =	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
    7.11  	Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML

     8.1 --- a/src/Cube/IsaMakefile	Tue May 06 15:24:41 1997 +0200
     8.2 +++ b/src/Cube/IsaMakefile	Tue May 06 15:27:35 1997 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  # IsaMakefile for Cube
     8.5  #
     8.6  
     8.7 -OUT = $(ISABELLE_OUTPUT_DIR)
     8.8 +OUT = $(ISABELLE_OUTPUT)
     8.9  FILES =	ROOT.ML Cube.thy Cube.ML
    8.10  
    8.11  $(OUT)/Cube: $(OUT)/Pure $(FILES)

     9.1 --- a/src/FOL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
     9.2 +++ b/src/FOL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
     9.3 @@ -4,7 +4,7 @@
     9.4  # IsaMakefile for FOL
     9.5  #
     9.6  
     9.7 -OUT = $(ISABELLE_OUTPUT_DIR)
     9.8 +OUT = $(ISABELLE_OUTPUT)
     9.9  
    9.10  FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    9.11  	thy_data.ML cladata.ML \

    10.1 --- a/src/FOLP/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    10.2 +++ b/src/FOLP/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    10.3 @@ -4,7 +4,7 @@
    10.4  # IsaMakefile for FOLP
    10.5  #
    10.6  
    10.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    10.8 +OUT = $(ISABELLE_OUTPUT)
    10.9  
   10.10  FILES =	ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
   10.11  	hypsubst.ML classical.ML simp.ML

    11.1 --- a/src/HOL/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    11.2 +++ b/src/HOL/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  
    11.5  #### Base system
    11.6  
    11.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    11.8 +OUT = $(ISABELLE_OUTPUT)
    11.9  
   11.10  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
   11.11  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \

    12.1 --- a/src/HOLCF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    12.2 +++ b/src/HOLCF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  
    12.5  #### Base system
    12.6  
    12.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    12.8 +OUT = $(ISABELLE_OUTPUT)
    12.9  
   12.10  THYS = Porder.thy Porder0.thy Pcpo.thy \
   12.11         Fun1.thy Fun2.thy Fun3.thy \

    13.1 --- a/src/LCF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    13.2 +++ b/src/LCF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    13.3 @@ -4,7 +4,7 @@
    13.4  # IsaMakefile for LCF
    13.5  #
    13.6  
    13.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    13.8 +OUT = $(ISABELLE_OUTPUT)
    13.9  FILES =	ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
   13.10  
   13.11  $(OUT)/LCF: $(OUT)/FOL $(FILES)

    14.1 --- a/src/Pure/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    14.2 +++ b/src/Pure/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    14.3 @@ -7,7 +7,7 @@
    14.4  # are loaded on top of it.
    14.5  #
    14.6  
    14.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    14.8 +OUT = $(ISABELLE_OUTPUT)
    14.9  
   14.10  FILES = ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
   14.11  	ML-Systems/smlnj-1.07.ML ML-Systems/smlnj-1.09.ML ROOT.ML \

    15.1 --- a/src/Pure/mk	Tue May 06 15:24:41 1997 +0200
    15.2 +++ b/src/Pure/mk	Tue May 06 15:27:35 1997 +0200
    15.3 @@ -32,4 +32,4 @@
    15.4    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
    15.5    -q RAW_ML_SYSTEM Pure
    15.6  
    15.7 -chmod -w $ISABELLE_OUTPUT_DIR/Pure
    15.8 +chmod -w $ISABELLE_OUTPUT/Pure

    16.1 --- a/src/Sequents/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    16.2 +++ b/src/Sequents/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    16.3 @@ -4,7 +4,7 @@
    16.4  # IsaMakefile for Sequents
    16.5  #
    16.6  
    16.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    16.8 +OUT = $(ISABELLE_OUTPUT)
    16.9  
   16.10  NAMES = ILL LK S4 S43 T
   16.11  FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)

    17.1 --- a/src/ZF/IsaMakefile	Tue May 06 15:24:41 1997 +0200
    17.2 +++ b/src/ZF/IsaMakefile	Tue May 06 15:27:35 1997 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  
    17.5  #### Base system
    17.6  
    17.7 -OUT = $(ISABELLE_OUTPUT_DIR)
    17.8 +OUT = $(ISABELLE_OUTPUT)
    17.9  
   17.10  NAMES = ZF upair subset pair domrange \
   17.11  	func AC equalities Bool \