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