equal
deleted
inserted
replaced
73 |
73 |
74 LOGIC="$1"; shift |
74 LOGIC="$1"; shift |
75 NAME="$1"; shift |
75 NAME="$1"; shift |
76 |
76 |
77 |
77 |
|
78 # prepare directories for html and graph output |
|
79 |
|
80 if [ $HTML = "true" -o $GRAPH = "true" ]; then |
|
81 if [ ! -d $ISABELLE_BROWSER_INFO/gif ]; then |
|
82 mkdir -p $ISABELLE_BROWSER_INFO/gif |
|
83 cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif |
|
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 |
|
94 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html |
|
95 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser |
|
96 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities |
|
97 cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G* |
|
98 cp $ISABELLE_HOME/lib/browser/a*/*.class $ISABELLE_BROWSER_INFO/graph/a* |
|
99 fi |
|
100 |
78 |
101 |
79 ## main |
102 ## main |
80 |
103 |
81 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
104 [ -z "$SESSION" ] && SESSION=$(basename $NAME) |
82 |
105 |
83 if [ -n "$BUILD" ]; then |
106 if [ -n "$BUILD" ]; then |
84 exec $ISABELLE \ |
107 exec $ISABELLE \ |
85 -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \ |
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;" \ |
86 -q -w $LOGIC $NAME |
109 -q -w $LOGIC $NAME |
87 else |
110 else |
88 exec $ISABELLE \ |
111 exec $ISABELLE \ |
89 -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \ |
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();" \ |
90 -r -q $LOGIC |
113 -r -q $LOGIC |
91 fi |
114 fi |