equal
deleted
inserted
replaced
30 echo " -u pass 'exit_use_dir\".\";' to the ML session" |
30 echo " -u pass 'exit_use_dir\".\";' to the ML session" |
31 echo |
31 echo |
32 echo " INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps." |
32 echo " INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps." |
33 echo " These are either names to be searched in the Isabelle path, or actual" |
33 echo " These are either names to be searched in the Isabelle path, or actual" |
34 echo " file names (then containing at least one /)." |
34 echo " file names (then containing at least one /)." |
35 echo " If INPUT is \"SYSTEM\", just start the bare bones ML system." |
35 echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." |
36 echo |
36 echo |
37 exit 1 |
37 exit 1 |
38 } |
38 } |
39 |
39 |
40 function fail() |
40 function fail() |
115 ## input heap file |
115 ## input heap file |
116 |
116 |
117 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC" |
117 [ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC" |
118 |
118 |
119 case "$INPUT" in |
119 case "$INPUT" in |
120 SYSTEM) |
120 RAW_ML_SYSTEM) |
121 INFILE="" |
121 INFILE="" |
122 ;; |
122 ;; |
123 */*) |
123 */*) |
124 INFILE="$INPUT" |
124 INFILE="$INPUT" |
125 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |
125 [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" |