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