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 (output heap image, use dir \".\")" |
18 echo " -b build mode (output heap image, use dir \".\")" |
19 echo " -c force copying of heap file (for Poly/ML)" |
19 echo " -c force copying of heap file (for Poly/ML)" |
|
20 echo " -g BOOL generate theory graph data (default false)" |
|
21 echo " -h BOOL generate theory HTML data (default false)" |
20 echo " -s NAME override session NAME" |
22 echo " -s NAME override session NAME" |
21 echo |
23 echo |
22 echo " Build object-logic or run examples. Also creates browsing" |
24 echo " Build object-logic or run examples. Also creates browsing" |
23 echo " information (HTML etc.) according to settings." |
25 echo " information (HTML etc.) according to settings." |
24 echo |
26 echo |
30 |
32 |
31 # options |
33 # options |
32 |
34 |
33 BUILD="" |
35 BUILD="" |
34 COPYDB="" |
36 COPYDB="" |
|
37 GRAPH=false |
|
38 HTML=false |
35 SESSION="" |
39 SESSION="" |
36 |
40 |
37 while getopts "bcs:" OPT |
41 function getoptions() |
38 do |
42 { |
39 case "$OPT" in |
43 OPTIND=1 |
40 b) |
44 while getopts "bcg:h:s:" OPT |
41 BUILD=true |
45 do |
42 ;; |
46 case "$OPT" in |
43 c) |
47 b) |
44 COPYDB="-c" |
48 BUILD=true |
45 ;; |
49 ;; |
46 s) |
50 c) |
47 SESSION="$OPTARG" |
51 COPYDB="-c" |
48 ;; |
52 ;; |
49 \?) |
53 g) |
50 usage |
54 GRAPH="$OPTARG" |
51 ;; |
55 ;; |
52 esac |
56 h) |
53 done |
57 HTML="$OPTARG" |
|
58 ;; |
|
59 s) |
|
60 SESSION="$OPTARG" |
|
61 ;; |
|
62 \?) |
|
63 usage |
|
64 ;; |
|
65 esac |
|
66 done |
|
67 } |
54 |
68 |
|
69 getoptions $ISABELLE_USEDIR_OPTIONS |
|
70 |
|
71 getoptions "$@" |
55 shift $(($OPTIND - 1)) |
72 shift $(($OPTIND - 1)) |
56 |
73 |
57 |
74 |
58 # args |
75 # args |
59 |
76 |
68 |
85 |
69 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
86 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
70 |
87 |
71 if [ -n "$BUILD" ]; then |
88 if [ -n "$BUILD" ]; then |
72 exec $ISABELLE \ |
89 exec $ISABELLE \ |
73 -e "make_html := $ISABELLE_HTML;" \ |
90 -e "make_html := $HTML;" \ |
74 -e "set_session\"$SESSION\";" \ |
91 -e "set_session\"$SESSION\";" \ |
75 -e "exit_use_dir\".\";" \ |
92 -e "exit_use_dir\".\";" \ |
76 -q $COPYDB $LOGIC $NAME |
93 -q $COPYDB $LOGIC $NAME |
77 else |
94 else |
78 exec $ISABELLE \ |
95 exec $ISABELLE \ |
79 -e "make_html := $ISABELLE_HTML;" \ |
96 -e "make_html := $HTML;" \ |
80 -e "set_session\"$SESSION\";" \ |
97 -e "set_session\"$SESSION\";" \ |
81 -e "exit_use_dir\"$NAME\"; quit();" \ |
98 -e "exit_use_dir\"$NAME\"; quit();" \ |
82 -r -q $LOGIC |
99 -r -q $LOGIC |
83 fi |
100 fi |