equal
deleted
inserted
replaced
15 echo "Usage: $PRG LOGIC NAME" |
15 echo "Usage: $PRG LOGIC NAME" |
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -B build mode with THIS_IS_ISABELLE_BUILD indication" |
18 echo " -B build mode with THIS_IS_ISABELLE_BUILD indication" |
19 echo " -P PATH set path for remote theory browsing information" |
19 echo " -P PATH set path for remote theory browsing information" |
|
20 echo " -c BOOL clean document source after build (default true)" |
20 echo " -b build mode (output heap image, using current dir)" |
21 echo " -b build mode (output heap image, using current dir)" |
|
22 echo " -d FORMAT build document as FORMAT (default false)" |
21 echo " -i BOOL generate theory browsing information," |
23 echo " -i BOOL generate theory browsing information," |
22 echo " i.e. HTML / graph data (default false)" |
24 echo " i.e. HTML / graph data (default false)" |
23 echo " -r reset session path" |
25 echo " -r reset session path" |
24 echo " -s NAME override session NAME" |
26 echo " -s NAME override session NAME" |
25 echo |
27 echo |
35 ## process command line |
37 ## process command line |
36 |
38 |
37 # options |
39 # options |
38 |
40 |
39 BUILD="" |
41 BUILD="" |
|
42 CLEANDOC=true |
|
43 DOCUMENT=false |
40 INFO=false |
44 INFO=false |
41 RESET=false |
45 RESET=false |
42 SESSION="" |
46 SESSION="" |
43 RPATH="" |
47 RPATH="" |
44 |
48 |
45 function getoptions() |
49 function getoptions() |
46 { |
50 { |
47 OPTIND=1 |
51 OPTIND=1 |
48 while getopts "BP:bi:rs:" OPT |
52 while getopts "BP:bc:d:i:rs:" OPT |
49 do |
53 do |
50 case "$OPT" in |
54 case "$OPT" in |
51 B) |
55 B) |
52 BUILD=true |
56 BUILD=true |
53 export THIS_IS_ISABELLE_BUILD=true |
57 export THIS_IS_ISABELLE_BUILD=true |
54 ;; |
58 ;; |
55 b) |
59 b) |
56 BUILD=true |
60 BUILD=true |
|
61 ;; |
|
62 c) |
|
63 CLEANDOC="$OPTARG" |
|
64 ;; |
|
65 d) |
|
66 DOCUMENT="$OPTARG" |
57 ;; |
67 ;; |
58 i) |
68 i) |
59 INFO="$OPTARG" |
69 INFO="$OPTARG" |
60 ;; |
70 ;; |
61 r) |
71 r) |
117 mkdir -p "$LOGDIR" |
127 mkdir -p "$LOGDIR" |
118 |
128 |
119 |
129 |
120 # run isabelle |
130 # run isabelle |
121 |
131 |
|
132 PARENT=$(basename "$LOGIC") |
|
133 |
|
134 [ -z "$BUILD" ] && cd "$NAME" |
|
135 |
|
136 if [ "$DOCUMENT" != false -a -d document -a -f document/root.tex ] |
|
137 then DOC="$DOCUMENT" |
|
138 else DOC=""; fi |
|
139 |
|
140 |
122 SECONDS=0 |
141 SECONDS=0 |
123 |
|
124 PARENT=$(basename "$LOGIC") |
|
125 |
142 |
126 if [ -n "$BUILD" ]; then |
143 if [ -n "$BUILD" ]; then |
127 ITEM="$SESSION" |
144 ITEM="$SESSION" |
128 echo "Building $ITEM ..." |
145 echo "Building $ITEM ..." |
129 LOG="$LOGDIR/$ITEM" |
146 LOG="$LOGDIR/$ITEM" |
130 |
147 |
131 $ISABELLE \ |
148 $ISABELLE \ |
132 -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\";" \ |
149 -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\";" \ |
133 -q -w $LOGIC $NAME > $LOG 2>&1 |
150 -q -w $LOGIC $NAME > $LOG 2>&1 |
134 RC=$? |
151 RC=$? |
135 else |
152 else |
136 ITEM=$(basename $LOGIC)-"$SESSION" |
153 ITEM=$(basename $LOGIC)-"$SESSION" |
137 echo "Running $ITEM ..." |
154 echo "Running $ITEM ..." |
138 LOG="$LOGDIR/$ITEM" |
155 LOG="$LOGDIR/$ITEM" |
139 |
156 |
140 cd "$NAME" |
|
141 $ISABELLE \ |
157 $ISABELLE \ |
142 -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \ |
158 -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \ |
143 -r -q $LOGIC > $LOG 2>&1 |
159 -r -q $LOGIC > $LOG 2>&1 |
144 RC=$? |
160 RC=$? |
145 cd .. |
161 cd .. |
146 fi |
162 fi |
147 |
163 |