equal
deleted
inserted
replaced
|
1 #!/bin/bash -norc |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # DESCRIPTION: build object-logic or run examples |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG=$(basename $0) |
|
11 |
|
12 function usage() |
|
13 { |
|
14 echo |
|
15 echo "Usage: $PRG LOGIC NAME" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -b build mode (output heap image, use dir \".\")" |
|
19 echo " -c force copying of heap file (for Poly/ML)" |
|
20 echo " -s NAME override session NAME" |
|
21 echo |
|
22 echo " Build object-logic or run examples. Also creates browsing" |
|
23 echo " information (HTML etc.) according to settings." |
|
24 echo |
|
25 exit 1 |
|
26 } |
|
27 |
|
28 |
|
29 ## process command line |
|
30 |
|
31 # options |
|
32 |
|
33 BUILD="" |
|
34 COPYDB="" |
|
35 SESSION="" |
|
36 |
|
37 while getopts "bc" OPT |
|
38 do |
|
39 case "$OPT" in |
|
40 b) |
|
41 BUILD=true |
|
42 ;; |
|
43 c) |
|
44 COPYDB="-c" |
|
45 ;; |
|
46 s) |
|
47 SESSION="$OPTARG" |
|
48 ;; |
|
49 \?) |
|
50 usage |
|
51 ;; |
|
52 esac |
|
53 done |
|
54 |
|
55 shift $(($OPTIND - 1)) |
|
56 |
|
57 |
|
58 # args |
|
59 |
|
60 [ $# -ne 2 ] && usage |
|
61 |
|
62 LOGIC="$1"; shift |
|
63 NAME="$1"; shift |
|
64 |
|
65 |
|
66 |
|
67 ## main |
|
68 |
|
69 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
|
70 |
|
71 if [ -n "$BUILD" ]; then |
|
72 exec $ISABELLE \ |
|
73 -e "make_html := $ISABELLE_HTML;" \ |
|
74 -e "set_session\"$SESSION\";" \ |
|
75 -e "exit_use_dir\".\";" \ |
|
76 -q $COPYDB $LOGIC $NAME |
|
77 else |
|
78 exec $ISABELLE \ |
|
79 -e "make_html := $ISABELLE_HTML;" \ |
|
80 -e "set_session\"$SESSION\";" \ |
|
81 -e "exit_use_dir\"$NAME\";" \ |
|
82 -r -q $LOGIC |
|
83 fi |