equal
deleted
inserted
replaced
29 echo " -I startup Isar interaction mode" |
29 echo " -I startup Isar interaction mode" |
30 echo " -P startup Proof General interaction mode" |
30 echo " -P startup Proof General interaction mode" |
31 echo " -S secure mode -- disallow critical operations" |
31 echo " -S secure mode -- disallow critical operations" |
32 echo " -X startup PGIP interaction mode" |
32 echo " -X startup PGIP interaction mode" |
33 echo " -W OUTPUT startup process wrapper, with messages going to OUTPUT stream" |
33 echo " -W OUTPUT startup process wrapper, with messages going to OUTPUT stream" |
34 echo " -c tell ML system to compress output image" |
|
35 echo " -e MLTEXT pass MLTEXT to the ML session" |
34 echo " -e MLTEXT pass MLTEXT to the ML session" |
36 echo " -f pass 'Session.finish();' to the ML session" |
35 echo " -f pass 'Session.finish();' to the ML session" |
37 echo " -m MODE add print mode for output" |
36 echo " -m MODE add print mode for output" |
38 echo " -q non-interactive session" |
37 echo " -q non-interactive session" |
39 echo " -r open heap file read-only" |
38 echo " -r open heap file read-only" |
62 ISAR=false |
61 ISAR=false |
63 PROOFGENERAL="" |
62 PROOFGENERAL="" |
64 SECURE="" |
63 SECURE="" |
65 WRAPPER_OUTPUT="" |
64 WRAPPER_OUTPUT="" |
66 PGIP="" |
65 PGIP="" |
67 COMPRESS="" |
|
68 MLTEXT="" |
66 MLTEXT="" |
69 MODES="" |
67 MODES="" |
70 TERMINATE="" |
68 TERMINATE="" |
71 READONLY="" |
69 READONLY="" |
72 NOWRITE="" |
70 NOWRITE="" |
73 |
71 |
74 while getopts "IPSW:Xce:fm:qruw" OPT |
72 while getopts "IPSW:Xe:fm:qruw" OPT |
75 do |
73 do |
76 case "$OPT" in |
74 case "$OPT" in |
77 I) |
75 I) |
78 ISAR=true |
76 ISAR=true |
79 ;; |
77 ;; |
86 W) |
84 W) |
87 WRAPPER_OUTPUT="$OPTARG" |
85 WRAPPER_OUTPUT="$OPTARG" |
88 ;; |
86 ;; |
89 X) |
87 X) |
90 PGIP=true |
88 PGIP=true |
91 ;; |
|
92 c) |
|
93 COMPRESS=true |
|
94 ;; |
89 ;; |
95 e) |
90 e) |
96 MLTEXT="$MLTEXT $OPTARG" |
91 MLTEXT="$MLTEXT $OPTARG" |
97 ;; |
92 ;; |
98 f) |
93 f) |
228 MLTEXT="$MLTEXT; Isar.main();" |
223 MLTEXT="$MLTEXT; Isar.main();" |
229 else |
224 else |
230 NICE="" |
225 NICE="" |
231 fi |
226 fi |
232 |
227 |
233 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP |
228 export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP |
234 |
229 |
235 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
230 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then |
236 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
231 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" |
237 else |
232 else |
238 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |
233 $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE" |