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