lib/Tools/mkdir
author wenzelm
Mon Apr 10 23:38:02 2000 +0200 (2000-04-10)
changeset 8685 05b6e5bcab66
parent 8579 81ef0fc80822
child 9237 161fb7f00414
permissions -rwxr-xr-x
handle dir prefix;
     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   DIR_NAME="$1"; shift
    75 elif [ $# -eq 2 ]; then
    76   LOGIC="$1"; shift
    77   DIR_NAME="$1"; shift
    78 else
    79   usage
    80 fi
    81 
    82 DIR=$(dirname "$DIR_NAME")
    83 NAME=$(basename "$DIR_NAME")
    84 
    85 
    86 ## main
    87 
    88 # IsaMakefile
    89 
    90 mkdir -p "$DIR" || fail "Bad directory: $DIR"
    91 cd "$DIR"
    92 
    93 
    94 DOCUMENT_ROOT=""
    95 
    96 if [ -n "$BUILD" ]; then
    97   IMAGES="$NAME"
    98   TEST=""
    99   TARGET="\$(OUT)/$NAME"
   100   ROOT_ML="ROOT.ML"
   101   SOURCES="*.thy"
   102   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
   103   USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
   104 else
   105   IMAGES=""
   106   TEST="$NAME"
   107   TARGET="\$(LOG)/$LOGIC-$NAME.gz"
   108   ROOT_ML="$NAME/ROOT.ML"
   109   SOURCES="$NAME/*.thy"
   110   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
   111   USEDIR="\$(USEDIR)"
   112 fi
   113 
   114 if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
   115   echo "keeping $PWD/$ISAMAKEFILE" >&2
   116 else
   117   { echo
   118     echo "## targets"
   119     echo
   120     echo "default: $NAME"
   121     echo "images: $IMAGES"
   122     echo "test: $TEST"
   123     echo
   124     echo "all: images test"
   125     echo
   126     echo
   127     echo "## global settings"
   128     echo
   129     echo "SRC = \$(ISABELLE_HOME)/src"
   130     echo "OUT = \$(ISABELLE_OUTPUT)"
   131     echo "LOG = \$(OUT)/log"
   132     echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
   133     echo
   134     echo
   135     echo "## $NAME"
   136     echo ""
   137     if [ -n "$PARENT" ]; then
   138       echo "$NAME: $LOGIC $TARGET"
   139       echo
   140       echo "$LOGIC:"
   141       echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
   142       echo
   143       echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
   144       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
   145     else
   146       echo "$NAME: $TARGET"
   147       echo
   148       echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
   149       echo -e "\t@$USEDIR $LOGIC $NAME"
   150     fi
   151     echo
   152     echo
   153     echo "## clean"
   154     echo
   155     echo "clean:"
   156     echo -e "\t@rm -f $TARGET"
   157     echo
   158   } | {
   159     if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
   160       cat
   161     else
   162       cat > "$ISAMAKEFILE"
   163     fi
   164   }
   165 fi
   166 
   167 
   168 # base directory
   169 
   170 if [ -z "$BUILD" ]; then
   171   mkdir -p "$NAME" || fail "Bad directory: $PWD/$NAME"
   172   cd "$NAME"
   173 fi
   174 
   175 if [ -f ROOT.ML ]; then
   176   echo "keeping $PWD/ROOT.ML" >&2
   177 else
   178   echo -e "\n(* use_thy \"YourTheory\"; *)\n" >ROOT.ML
   179 fi
   180 
   181 
   182 # document directory
   183 
   184 if [ -n "$DOCUMENT" ]; then
   185   if [ -e document ]; then
   186     echo "keeping $PWD/document" >&2
   187   else
   188     mkdir document || fail "Bad directory: $PWD/document"
   189     cat >document/root.tex <<EOF
   190 
   191 \documentclass[11pt,a4paper]{article}
   192 \usepackage{isabelle,isabellesym,pdfsetup}
   193 
   194 \begin{document}
   195 \input{session}
   196 \end{document}
   197 
   198 EOF
   199   fi
   200 fi