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