equal
deleted
inserted
replaced
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, use dir \".\")" |
19 echo " -g BOOL generate theory graph data (default false)" |
19 echo " -i BOOL generate theory browsing information," |
20 echo " -h BOOL generate theory HTML data (default false)" |
20 echo " i.e. HTML / graph data (default false)" |
21 echo " -s NAME override session NAME" |
21 echo " -s NAME override session NAME" |
22 echo |
22 echo |
23 echo " Build object-logic or run examples. Also creates browsing" |
23 echo " Build object-logic or run examples. Also creates browsing" |
24 echo " information (HTML etc.) according to settings." |
24 echo " information (HTML etc.) according to settings." |
25 echo |
25 echo |
30 ## process command line |
30 ## process command line |
31 |
31 |
32 # options |
32 # options |
33 |
33 |
34 BUILD="" |
34 BUILD="" |
35 GRAPH=false |
35 INFO=false |
36 HTML=false |
|
37 SESSION="" |
36 SESSION="" |
38 |
37 |
39 function getoptions() |
38 function getoptions() |
40 { |
39 { |
41 OPTIND=1 |
40 OPTIND=1 |
42 while getopts "bcg:h:s:" OPT |
41 while getopts "bi:s:" OPT |
43 do |
42 do |
44 case "$OPT" in |
43 case "$OPT" in |
45 b) |
44 b) |
46 BUILD=true |
45 BUILD=true |
47 ;; |
46 ;; |
48 g) |
47 i) |
49 GRAPH="$OPTARG" |
48 INFO="$OPTARG" |
50 ;; |
|
51 h) |
|
52 HTML="$OPTARG" |
|
53 ;; |
49 ;; |
54 s) |
50 s) |
55 SESSION="$OPTARG" |
51 SESSION="$OPTARG" |
56 ;; |
52 ;; |
57 \?) |
53 \?) |
75 NAME="$1"; shift |
71 NAME="$1"; shift |
76 |
72 |
77 |
73 |
78 # prepare directories for html and graph output |
74 # prepare directories for html and graph output |
79 |
75 |
80 if [ $HTML = "true" -o $GRAPH = "true" ]; then |
76 if [ $INFO = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then |
81 if [ ! -d $ISABELLE_BROWSER_INFO/gif ]; then |
77 mkdir -p $ISABELLE_BROWSER_INFO/gif |
82 mkdir -p $ISABELLE_BROWSER_INFO/gif |
78 cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif |
83 cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif |
79 cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html |
84 fi |
|
85 fi |
|
86 |
|
87 if [ $HTML = "true" -a ! -d $ISABELLE_BROWSER_INFO/html ]; then |
|
88 mkdir -p $ISABELLE_BROWSER_INFO/html |
|
89 cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/html/index.html |
|
90 fi |
|
91 |
|
92 if [ $GRAPH = "true" -a ! -d $ISABELLE_BROWSER_INFO/graph ]; then |
|
93 mkdir -p $ISABELLE_BROWSER_INFO/graph |
80 mkdir -p $ISABELLE_BROWSER_INFO/graph |
94 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html |
81 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html |
95 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser |
82 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser |
96 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities |
83 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities |
97 cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G* |
84 cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G* |
103 |
90 |
104 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
91 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
105 |
92 |
106 if [ -n "$BUILD" ]; then |
93 if [ -n "$BUILD" ]; then |
107 exec $ISABELLE \ |
94 exec $ISABELLE \ |
108 -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \ |
95 -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \ |
109 -q -w $LOGIC $NAME |
96 -q -w $LOGIC $NAME |
110 else |
97 else |
111 exec $ISABELLE \ |
98 exec $ISABELLE \ |
112 -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \ |
99 -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \ |
113 -r -q $LOGIC |
100 -r -q $LOGIC |
114 fi |
101 fi |