equal
deleted
inserted
replaced
20 echo " -D PATH dump generated document sources into PATH" |
20 echo " -D PATH dump generated document sources into PATH" |
21 echo " -P PATH set path for remote theory browsing information" |
21 echo " -P PATH set path for remote theory browsing information" |
22 echo " -b build mode (output heap image, using current dir)" |
22 echo " -b build mode (output heap image, using current dir)" |
23 echo " -c BOOL tell ML system to compress output image (default true)" |
23 echo " -c BOOL tell ML system to compress output image (default true)" |
24 echo " -d FORMAT build document as FORMAT (default false)" |
24 echo " -d FORMAT build document as FORMAT (default false)" |
25 echo " -i BOOL generate theory browsing information," |
25 echo " -i BOOL generate theory browser information (default false)" |
26 echo " i.e. HTML / graph data (default false)" |
26 echo " -m MODE add print mode for output" |
27 echo " -r reset session path" |
27 echo " -r reset session path" |
28 echo " -s NAME override session NAME" |
28 echo " -s NAME override session NAME" |
29 echo |
29 echo |
30 echo " Build object-logic or run examples. Also creates browsing" |
30 echo " Build object-logic or run examples. Also creates browsing" |
31 echo " information (HTML etc.) according to settings." |
31 echo " information (HTML etc.) according to settings." |
44 RPATH="" |
44 RPATH="" |
45 BUILD="" |
45 BUILD="" |
46 COMPRESS=true |
46 COMPRESS=true |
47 DOCUMENT=false |
47 DOCUMENT=false |
48 INFO=false |
48 INFO=false |
|
49 MODES="" |
49 RESET=false |
50 RESET=false |
50 SESSION="" |
51 SESSION="" |
51 |
52 |
52 function getoptions() |
53 function getoptions() |
53 { |
54 { |
54 OPTIND=1 |
55 OPTIND=1 |
55 while getopts "D:P:bc:d:i:rs:" OPT |
56 while getopts "D:P:bc:d:i:m:rs:" OPT |
56 do |
57 do |
57 case "$OPT" in |
58 case "$OPT" in |
58 D) |
59 D) |
59 DUMP="$OPTARG" |
60 DUMP="$OPTARG" |
60 ;; |
61 ;; |
70 d) |
71 d) |
71 DOCUMENT="$OPTARG" |
72 DOCUMENT="$OPTARG" |
72 ;; |
73 ;; |
73 i) |
74 i) |
74 INFO="$OPTARG" |
75 INFO="$OPTARG" |
|
76 ;; |
|
77 m) |
|
78 if [ -z "$MODES" ]; then |
|
79 MODES="\"$OPTARG\"" |
|
80 else |
|
81 MODES="$MODES, \"$OPTARG\"" |
|
82 fi |
75 ;; |
83 ;; |
76 r) |
84 r) |
77 RESET=true |
85 RESET=true |
78 ;; |
86 ;; |
79 s) |
87 s) |
143 |
151 |
144 OPT_C="" |
152 OPT_C="" |
145 [ "$COMPRESS" = true ] && OPT_C="-c" |
153 [ "$COMPRESS" = true ] && OPT_C="-c" |
146 |
154 |
147 "$ISABELLE" \ |
155 "$ISABELLE" \ |
148 -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \ |
156 -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \ |
149 $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1 |
157 $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1 |
150 RC="$?" |
158 RC="$?" |
151 else |
159 else |
152 ITEM=$(basename "$LOGIC")-"$SESSION" |
160 ITEM=$(basename "$LOGIC")-"$SESSION" |
153 echo "Running $ITEM ..." |
161 echo "Running $ITEM ..." |
154 LOG="$LOGDIR/$ITEM" |
162 LOG="$LOGDIR/$ITEM" |
155 |
163 |
156 "$ISABELLE" \ |
164 "$ISABELLE" \ |
157 -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \ |
165 -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \ |
158 -r -q "$LOGIC" > "$LOG" 2>&1 |
166 -r -q "$LOGIC" > "$LOG" 2>&1 |
159 RC="$?" |
167 RC="$?" |
160 cd .. |
168 cd .. |
161 fi |
169 fi |
162 |
170 |