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