equal
deleted
inserted
replaced
92 if [ -n "$BUILD" ]; then |
92 if [ -n "$BUILD" ]; then |
93 IMAGES="$NAME" |
93 IMAGES="$NAME" |
94 TEST="" |
94 TEST="" |
95 TARGET="\$(OUT)/$NAME" |
95 TARGET="\$(OUT)/$NAME" |
96 ROOT_ML="ROOT.ML" |
96 ROOT_ML="ROOT.ML" |
|
97 SOURCES="*.thy" |
97 [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex" |
98 [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex" |
98 USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library" |
99 USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library" |
99 else |
100 else |
100 IMAGES="" |
101 IMAGES="" |
101 TEST="$NAME" |
102 TEST="$NAME" |
102 TARGET="\$(LOG)/$LOGIC-$NAME.gz" |
103 TARGET="\$(LOG)/$LOGIC-$NAME.gz" |
103 ROOT_ML="$NAME/ROOT.ML" |
104 ROOT_ML="$NAME/ROOT.ML" |
|
105 SOURCES="$NAME/*.thy" |
104 [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex" |
106 [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex" |
105 USEDIR="\$(USEDIR)" |
107 USEDIR="\$(USEDIR)" |
106 fi |
108 fi |
107 |
109 |
108 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then |
110 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then |
132 echo "$NAME: $LOGIC $TARGET" |
134 echo "$NAME: $LOGIC $TARGET" |
133 echo |
135 echo |
134 echo "$LOGIC:" |
136 echo "$LOGIC:" |
135 echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC" |
137 echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC" |
136 echo |
138 echo |
137 echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## add $NAME sources here" |
139 echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES" |
138 echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME" |
140 echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME" |
139 else |
141 else |
140 echo "$NAME: $TARGET" |
142 echo "$NAME: $TARGET" |
141 echo |
143 echo |
142 echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT ## add $NAME sources here" |
144 echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT ## $SOURCES" |
143 echo -e "\t@$USEDIR $LOGIC $NAME" |
145 echo -e "\t@$USEDIR $LOGIC $NAME" |
144 fi |
146 fi |
145 echo |
147 echo |
146 echo |
148 echo |
147 echo "## clean" |
149 echo "## clean" |