added symbolinput filter;
authorwenzelm
Mon Dec 16 09:59:18 1996 +0100 (1996-12-16)
changeset 24004b08766bc9d1
parent 2399 6719b465198b
child 2401 0293bc1cecfc
added symbolinput filter;
lib/scripts/run-polyml
     1.1 --- a/lib/scripts/run-polyml	Mon Dec 16 09:58:16 1996 +0100
     1.2 +++ b/lib/scripts/run-polyml	Mon Dec 16 09:59:18 1996 +0100
     1.3 @@ -17,9 +17,8 @@
     1.4  }
     1.5  
     1.6  
     1.7 -## locations and settings
     1.8 +## Poly/ML programs
     1.9  
    1.10 -ML_DBASE=$ML_HOME/ML_dbase
    1.11  POLY=$ML_HOME/poly
    1.12  DISCGARB=$ML_HOME/discgarb
    1.13  
    1.14 @@ -35,7 +34,7 @@
    1.15  MLINIT=""
    1.16  
    1.17  if [ -z "$INFILE" ]; then
    1.18 -  INFILE="$ML_DBASE"
    1.19 +  INFILE="$ML_HOME/ML_dbase"
    1.20    MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();"
    1.21  fi
    1.22  
    1.23 @@ -60,22 +59,19 @@
    1.24  ## run it!
    1.25  
    1.26  START_POLY="$POLY $ML_OPTIONS $DB"
    1.27 -DB_INFO=$(ls -l $DB)
    1.28 +DB_INFO=$(ls -l "$DB")
    1.29  
    1.30  [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"
    1.31  
    1.32  if [ -n "$TERMINATE" ]; then
    1.33    echo "$MLTEXT" | $START_POLY
    1.34    RC=$?
    1.35 -elif [ -z "$MLTEXT" ]; then
    1.36 -  $START_POLY
    1.37 -  RC=$?
    1.38  else
    1.39 -  { echo "$MLTEXT"; $ISABELLE_HOME/lib/scripts/ucat } | $START_POLY
    1.40 +  { echo "$MLTEXT"; $ISABELLE_HOME/lib/Tools/symbolinput } | $START_POLY
    1.41    RC=$?
    1.42  fi
    1.43  
    1.44 -NEW_DB_INFO=$(ls -l $DB)
    1.45 +NEW_DB_INFO=$(ls -l "$DB")
    1.46  [ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
    1.47  
    1.48  exit $RC