lib/Tools/mkdir
changeset 8244 c587f5ac4a98
parent 8211 714f164f0385
child 8289 5b288a96bc61
equal deleted inserted replaced
8243:5db67376df7d 8244:c587f5ac4a98
    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"