equal
deleted
inserted
replaced
94 |
94 |
95 mkdir -p "$DIR" || fail "Bad directory: $DIR" |
95 mkdir -p "$DIR" || fail "Bad directory: $DIR" |
96 cd "$DIR" |
96 cd "$DIR" |
97 |
97 |
98 DOCUMENT_ROOT="" |
98 DOCUMENT_ROOT="" |
|
99 VERBOSE="" |
|
100 [ -z "$QUIET" ] && VERBOSE="-v true " |
99 |
101 |
100 if [ -n "$BUILD" ]; then |
102 if [ -n "$BUILD" ]; then |
101 IMAGES="$NAME" |
103 IMAGES="$NAME" |
102 TEST="" |
104 TEST="" |
103 TARGET="\$(OUT)/$NAME" |
105 TARGET="\$(OUT)/$NAME" |
134 echo |
136 echo |
135 echo "SRC = \$(ISABELLE_HOME)/src" |
137 echo "SRC = \$(ISABELLE_HOME)/src" |
136 echo "OUT = \$(ISABELLE_OUTPUT)" |
138 echo "OUT = \$(ISABELLE_OUTPUT)" |
137 echo "LOG = \$(OUT)/log" |
139 echo "LOG = \$(OUT)/log" |
138 echo |
140 echo |
139 echo "USEDIR = \$(ISATOOL) usedir -v true -i true -d dvi ## -D document" |
141 echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi ## -D document" |
140 echo |
142 echo |
141 echo |
143 echo |
142 echo "## $NAME" |
144 echo "## $NAME" |
143 echo "" |
145 echo "" |
144 if [ -n "$PARENT" ]; then |
146 if [ -n "$PARENT" ]; then |
264 |
266 |
265 * 'isatool make' processes the session (including document preparation) |
267 * 'isatool make' processes the session (including document preparation) |
266 |
268 |
267 * $DIR/IsaMakefile contains compilation options and file dependencies |
269 * $DIR/IsaMakefile contains compilation options and file dependencies |
268 |
270 |
|
271 * $PREFIX/document/root.tex contains the LaTeX master document setup |
|
272 |
269 * $PREFIX/ROOT.ML needs to contain ML code to load all theories |
273 * $PREFIX/ROOT.ML needs to contain ML code to load all theories |
270 |
274 |
271 * $PREFIX/document/root.tex contains the LaTeX master document setup |
|
272 |
|
273 EOF |
275 EOF |
274 fi |
276 fi |