equal
deleted
inserted
replaced
13 { |
13 { |
14 echo |
14 echo |
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 (output heap image, use dir \".\")" |
18 echo " -b build mode (output heap image, using current dir)" |
19 echo " -i BOOL generate theory browsing information," |
19 echo " -i BOOL generate theory browsing information," |
20 echo " i.e. HTML / graph data (default false)" |
20 echo " i.e. HTML / graph data (default false)" |
|
21 echo " -r reset session path" |
21 echo " -s NAME override session NAME" |
22 echo " -s NAME override session NAME" |
22 echo |
23 echo |
23 echo " Build object-logic or run examples. Also creates browsing" |
24 echo " Build object-logic or run examples. Also creates browsing" |
24 echo " information (HTML etc.) according to settings." |
25 echo " information (HTML etc.) according to settings." |
25 echo |
26 echo |
31 |
32 |
32 # options |
33 # options |
33 |
34 |
34 BUILD="" |
35 BUILD="" |
35 INFO=false |
36 INFO=false |
|
37 RESET=false |
36 SESSION="" |
38 SESSION="" |
37 |
39 |
38 function getoptions() |
40 function getoptions() |
39 { |
41 { |
40 OPTIND=1 |
42 OPTIND=1 |
41 while getopts "bi:s:" OPT |
43 while getopts "bi:rs:" OPT |
42 do |
44 do |
43 case "$OPT" in |
45 case "$OPT" in |
44 b) |
46 b) |
45 BUILD=true |
47 BUILD=true |
46 ;; |
48 ;; |
47 i) |
49 i) |
48 INFO="$OPTARG" |
50 INFO="$OPTARG" |
|
51 ;; |
|
52 r) |
|
53 RESET=true |
49 ;; |
54 ;; |
50 s) |
55 s) |
51 SESSION="$OPTARG" |
56 SESSION="$OPTARG" |
52 ;; |
57 ;; |
53 \?) |
58 \?) |
110 ITEM="$SESSION" |
115 ITEM="$SESSION" |
111 echo -n "Building $ITEM ... " |
116 echo -n "Building $ITEM ... " |
112 LOG="$LOGDIR/$ITEM" |
117 LOG="$LOGDIR/$ITEM" |
113 |
118 |
114 $ISABELLE \ |
119 $ISABELLE \ |
115 -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \ |
120 -e "Session.use_dir $RESET $INFO \"$SESSION\";" \ |
116 -q -w $LOGIC $NAME > $LOG 2>&1 |
121 -q -w $LOGIC $NAME > $LOG 2>&1 |
117 else |
122 else |
118 ITEM=$(basename $LOGIC)-"$SESSION" |
123 ITEM=$(basename $LOGIC)-"$SESSION" |
119 echo -n "Running $ITEM ... " |
124 echo -n "Running $ITEM ... " |
120 LOG="$LOGDIR/$ITEM" |
125 LOG="$LOGDIR/$ITEM" |
121 |
126 |
|
127 cd "$NAME" |
122 $ISABELLE \ |
128 $ISABELLE \ |
123 -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \ |
129 -e "Session.use_dir $RESET $INFO \"$SESSION\"; quit();" \ |
124 -r -q $LOGIC > $LOG 2>&1 |
130 -r -q $LOGIC > $LOG 2>&1 |
|
131 cd .. |
125 fi |
132 fi |
126 |
133 |
127 RC=$? |
134 RC=$? |
128 |
135 |
129 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS) |
136 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS) |