equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
|
3 |
3 # $Id$ |
4 # $Id$ |
|
5 |
4 # Author: Markus Wenzel, TU Muenchen |
6 # Author: Markus Wenzel, TU Muenchen |
|
7 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # |
8 # |
6 # Isabelle process startup script. |
9 # Isabelle process startup script. |
7 |
10 |
8 |
11 |
9 ## settings |
12 ## settings |
28 echo |
31 echo |
29 echo " Options are:" |
32 echo " Options are:" |
30 echo " -C tell ML system to copy output image" |
33 echo " -C tell ML system to copy output image" |
31 echo " -I startup Isar interaction mode" |
34 echo " -I startup Isar interaction mode" |
32 echo " -P startup Proof General interaction mode" |
35 echo " -P startup Proof General interaction mode" |
33 echo " -X startup PGIP interaction mode" |
|
34 echo " -c tell ML system to compress output image" |
36 echo " -c tell ML system to compress output image" |
35 echo " -e MLTEXT pass MLTEXT to the ML session" |
37 echo " -e MLTEXT pass MLTEXT to the ML session" |
36 echo " -f pass 'Session.finish();' to the ML session" |
38 echo " -f pass 'Session.finish();' to the ML session" |
37 echo " -m MODE add print mode for output" |
39 echo " -m MODE add print mode for output" |
38 echo " -q non-interactive session" |
40 echo " -q non-interactive session" |
67 MODES="" |
69 MODES="" |
68 TERMINATE="" |
70 TERMINATE="" |
69 READONLY="" |
71 READONLY="" |
70 NOWRITE="" |
72 NOWRITE="" |
71 |
73 |
72 while getopts "XCIPce:fm:qruw" OPT |
74 while getopts "CIPce:fm:qruw" OPT |
73 do |
75 do |
74 case "$OPT" in |
76 case "$OPT" in |
75 C) |
77 C) |
76 COPYDB=true |
78 COPYDB=true |
77 ;; |
79 ;; |
78 I) |
80 I) |
79 ISAR=true |
81 ISAR=true |
80 ;; |
82 ;; |
81 P) |
83 P) |
82 PROOFGENERAL=true |
84 PROOFGENERAL=true |
83 ;; |
|
84 X) |
|
85 PGIP=true |
|
86 ;; |
85 ;; |
87 c) |
86 c) |
88 COMPRESS=true |
87 COMPRESS=true |
89 ;; |
88 ;; |
90 e) |
89 e) |
207 |
206 |
208 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
207 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
209 |
208 |
210 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
209 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
211 |
210 |
212 if [ -n "$PGIP" ]; then |
211 if [ -n "$PROOFGENERAL" ]; then |
213 MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;" |
|
214 elif [ -n "$PROOFGENERAL" ]; then |
|
215 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
212 MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" |
216 elif [ "$ISAR" = true ]; then |
213 elif [ "$ISAR" = true ]; then |
217 MLTEXT="$MLTEXT; Isar.main();" |
214 MLTEXT="$MLTEXT; Isar.main();" |
218 fi |
215 fi |
219 |
216 |