# HG changeset patch
# User wenzelm
# Date 1128795331 -7200
# Node ID 4a34fd6884b12df47317643d277092e5be97a3f4
# Parent  f4453001cbde281b15345e759c10bd9d92436b95
support ML_SUFFIX;

diff -r f4453001cbde -r 4a34fd6884b1 bin/isabelle-process
--- a/bin/isabelle-process	Sat Oct 08 18:51:03 2005 +0200
+++ b/bin/isabelle-process	Sat Oct 08 20:15:31 2005 +0200
@@ -153,7 +153,7 @@
     INFILE=""
     ;;
   */*)
-    INFILE="$INPUT"
+    INFILE="$INPUT$ML_SUFFIX"
     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
     ;;
   *)
@@ -166,7 +166,7 @@
     do
       DIR="$DIR/$ML_IDENTIFIER"
       ISA_PATH="$ISA_PATH  $DIR\n"
-      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+      [ -z "$INFILE" -a -f "$DIR/$INPUT$ML_SUFFIX" ] && INFILE="$DIR/$INPUT$ML_SUFFIX"
     done
     IFS="$ORIG_IFS"
 
@@ -186,11 +186,11 @@
     [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
     ;;
   */*)
-    OUTFILE="$OUTPUT"
+    OUTFILE="$OUTPUT$ML_SUFFIX"
     ;;
   *)
     mkdir -p "$ISABELLE_OUTPUT"
-    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT$ML_SUFFIX"
     ;;
 esac
 
@@ -199,7 +199,7 @@
 
 [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
 ISABELLE_PID="$$"
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX${ISABELLE_PID}"
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
 mkdir -p "$ISABELLE_TMP"
 
 
diff -r f4453001cbde -r 4a34fd6884b1 lib/Tools/findlogics
--- a/lib/Tools/findlogics	Sat Oct 08 18:51:03 2005 +0200
+++ b/lib/Tools/findlogics	Sat Oct 08 20:15:31 2005 +0200
@@ -34,7 +34,7 @@
   for FILE in "$DIR"/*
   do
     if [ -f "$FILE" ]; then
-      NAME=$(basename "$FILE")
+      NAME=$(basename "$FILE" "$ML_SUFFIX")
       LOGICS="$LOGICS $NAME"
     fi
   done