lib/Tools/mkdir
author wenzelm
Sat Feb 05 16:59:50 2000 +0100 (2000-02-05)
changeset 8198 73a5877ca517
parent 8194 0c5d9d23b715
child 8199 9e45cf2e6cf7
permissions -rwxr-xr-x
-I option;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # DESCRIPTION: prepare logic session directory
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG=$(basename $0)
    11 
    12 function usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [LOGIC] NAME"
    16   echo
    17   echo "  Options are:"
    18   echo "    -I FILE      alternative IsaMakefile output"
    19   echo "    -b           setup build mode (session outputs heap image)"
    20   echo "    -d           setup document"
    21   echo "    -p           include parent logic target"
    22   echo
    23   echo "  Prepare session directory, including IsaMakefile, document etc."
    24   echo "  with parent LOGIC (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
    25   echo
    26   exit 1
    27 }
    28 
    29 function fail()
    30 {
    31   echo "$1" >&2
    32   exit 2
    33 }
    34 
    35 
    36 ## process command line
    37 
    38 # options
    39 
    40 ISAMAKEFILE="IsaMakefile"
    41 BUILD=""
    42 DOCUMENT=""
    43 PARENT=""
    44 
    45 while getopts "I:bdp" OPT
    46 do
    47   case "$OPT" in
    48     I)
    49       ISAMAKEFILE="$OPTARG"
    50       ;;
    51     b)
    52       BUILD=true
    53       ;;
    54     d)
    55       DOCUMENT=true
    56       ;;
    57     p)
    58       PARENT=true
    59       ;;
    60     \?)
    61       usage
    62       ;;
    63   esac
    64 done
    65 
    66 shift $(($OPTIND - 1))
    67 
    68 
    69 # args
    70 
    71 
    72 if [ $# -eq 1 ]; then
    73   LOGIC="$ISABELLE_LOGIC"
    74   NAME="$1"; shift
    75 elif [ $# -eq 2 ]; then
    76   LOGIC="$1"; shift
    77   NAME="$1"; shift
    78 else
    79   usage
    80 fi
    81 
    82 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
    83 
    84 
    85 
    86 ## main
    87 
    88 # IsaMakefile
    89 
    90 if [ -n "$BUILD" ]; then
    91   IMAGES="$NAME"
    92   TEST=""
    93   TARGET="\$(OUT)/$NAME"
    94   USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
    95 else
    96   IMAGES=""
    97   TEST="$NAME"
    98   TARGET="\$(LOG)/$NAME.gz"
    99   USEDIR="\$(USEDIR)"
   100 fi
   101 
   102 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
   103   echo "keeping $PWD/$ISAMAKEFILE" >&2
   104 else
   105   { echo
   106     echo "## targets"
   107     echo
   108     echo "default: $NAME"
   109     echo "images: $IMAGES"
   110     echo "test: $TEST"
   111     echo
   112     echo "all: images test"
   113     echo
   114     echo
   115     echo "## global settings"
   116     echo
   117     echo "SRC = \$(ISABELLE_HOME)/src"
   118     echo "OUT = \$(ISABELLE_OUTPUT)"
   119     echo "LOG = \$(OUT)/log"
   120     echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi"
   121     echo
   122     echo
   123     echo "## $NAME"
   124     echo ""
   125     if [ -n "$PARENT" ]; then
   126       echo "$NAME: $LOGIC $TARGET"
   127       echo
   128       echo "$LOGIC:"
   129       echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
   130       echo
   131       echo "$TARGET: \$(OUT)/$LOGIC     ## add $NAME sources here"
   132       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
   133     else
   134       echo "$NAME: $TARGET"
   135       echo
   136       echo "$TARGET:                    ## add $NAME sources here"
   137       echo -e "\t@$USEDIR $LOGIC $NAME"
   138     fi
   139     echo
   140     echo
   141     echo "## clean"
   142     echo
   143     echo "clean:"
   144     echo -e "\t@rm -f $TARGET"
   145     echo
   146   } | {
   147     if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
   148       cat
   149     else
   150       cat > "$ISAMAKEFILE"
   151     fi
   152   }
   153 fi
   154 
   155 
   156 # base directory
   157 
   158 if [ -z "$BUILD" ]; then
   159   mkdir -p "$NAME" || fail "Bad directory: $PWD/$NAME"
   160   cd "$NAME"
   161 fi
   162 
   163 if [ -f ROOT.ML ]; then
   164   echo "keeping $PWD/ROOT.ML" >&2
   165 else
   166   echo -e "\n(* use_thy \"YourTheory\"; *)\n" >ROOT.ML
   167 fi
   168 
   169 
   170 # document directory
   171 
   172 if [ -n "$DOCUMENT" ]; then
   173   if [ -e document ]; then
   174     echo "keeping $PWD/document" >&2
   175   else
   176     mkdir document || fail "Bad directory: $PWD/document"
   177     cat >document/root.tex <<EOF
   178 
   179 \documentclass[11pt,a4paper]{article}
   180 \usepackage{isabelle,isabellesym,pdfsetup}
   181 
   182 \begin{document}
   183 \input{session}
   184 \end{document}
   185 
   186 EOF
   187   fi
   188 fi