lib/Tools/mkdir
author wenzelm
Thu Mar 16 00:32:55 2000 +0100 (2000-03-16)
changeset 8488 58e37d59c146
parent 8475 deb604b3d9a9
child 8501 2ff3d25943f1
permissions -rwxr-xr-x
do not change parindent/parskip;
     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 "    -P           include parent logic target"
    20   echo "    -b           setup build mode (session outputs heap image)"
    21   echo "    -d           setup document"
    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 PARENT=""
    42 BUILD=""
    43 DOCUMENT=""
    44 
    45 while getopts "I:Pbd" OPT
    46 do
    47   case "$OPT" in
    48     I)
    49       ISAMAKEFILE="$OPTARG"
    50       ;;
    51     P)
    52       PARENT=true
    53       ;;
    54     b)
    55       BUILD=true
    56       ;;
    57     d)
    58       DOCUMENT=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 DOCUMENT_ROOT=""
    91 
    92 if [ -n "$BUILD" ]; then
    93   IMAGES="$NAME"
    94   TEST=""
    95   TARGET="\$(OUT)/$NAME"
    96   ROOT_ML="ROOT.ML"
    97   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
    98   USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
    99 else
   100   IMAGES=""
   101   TEST="$NAME"
   102   TARGET="\$(LOG)/$LOGIC-$NAME.gz"
   103   ROOT_ML="$NAME/ROOT.ML"
   104   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
   105   USEDIR="\$(USEDIR)"
   106 fi
   107 
   108 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
   109   echo "keeping $PWD/$ISAMAKEFILE" >&2
   110 else
   111   { echo
   112     echo "## targets"
   113     echo
   114     echo "default: $NAME"
   115     echo "images: $IMAGES"
   116     echo "test: $TEST"
   117     echo
   118     echo "all: images test"
   119     echo
   120     echo
   121     echo "## global settings"
   122     echo
   123     echo "SRC = \$(ISABELLE_HOME)/src"
   124     echo "OUT = \$(ISABELLE_OUTPUT)"
   125     echo "LOG = \$(OUT)/log"
   126     echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
   127     echo
   128     echo
   129     echo "## $NAME"
   130     echo ""
   131     if [ -n "$PARENT" ]; then
   132       echo "$NAME: $LOGIC $TARGET"
   133       echo
   134       echo "$LOGIC:"
   135       echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
   136       echo
   137       echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
   138       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
   139     else
   140       echo "$NAME: $TARGET"
   141       echo
   142       echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
   143       echo -e "\t@$USEDIR $LOGIC $NAME"
   144     fi
   145     echo
   146     echo
   147     echo "## clean"
   148     echo
   149     echo "clean:"
   150     echo -e "\t@rm -f $TARGET"
   151     echo
   152   } | {
   153     if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
   154       cat
   155     else
   156       cat > "$ISAMAKEFILE"
   157     fi
   158   }
   159 fi
   160 
   161 
   162 # base directory
   163 
   164 if [ -z "$BUILD" ]; then
   165   mkdir -p "$NAME" || fail "Bad directory: $PWD/$NAME"
   166   cd "$NAME"
   167 fi
   168 
   169 if [ -f ROOT.ML ]; then
   170   echo "keeping $PWD/ROOT.ML" >&2
   171 else
   172   echo -e "\n(* use_thy \"YourTheory\"; *)\n" >ROOT.ML
   173 fi
   174 
   175 
   176 # document directory
   177 
   178 if [ -n "$DOCUMENT" ]; then
   179   if [ -e document ]; then
   180     echo "keeping $PWD/document" >&2
   181   else
   182     mkdir document || fail "Bad directory: $PWD/document"
   183     cat >document/root.tex <<EOF
   184 
   185 \documentclass[11pt,a4paper]{article}
   186 \usepackage{isabelle,isabellesym,pdfsetup}
   187 
   188 \renewcommand{\isamarkupheader}[1]{\section{#1}}
   189 
   190 \begin{document}
   191 \input{session}
   192 \end{document}
   193 
   194 EOF
   195   fi
   196 fi