lib/Tools/mkdir
author paulson
Tue, 02 Feb 2010 09:48:20 +0000
changeset 35503 7bba12c3b7b6
parent 32299 5f33ce0ed21f
child 40895 c3f68ea97495
permissions -rwxr-xr-x
Correction of a tiny error
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10555
2323ec838401 /usr/bin/env bash;
wenzelm
parents: 10511
diff changeset
     1
#!/usr/bin/env bash
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
     2
#
9788
wenzelm
parents: 9656
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
8159
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
10511
wenzelm
parents: 10423
diff changeset
    10
PRG="$(basename "$0")"
8159
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
28650
a7ba12e0d3b7 tuned usage line;
wenzelm
parents: 28504
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [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:"
8198
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
    18
  echo "    -I FILE      alternative IsaMakefile output"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
    19
  echo "    -P           include parent logic target"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    20
  echo "    -b           setup build mode (session outputs heap image)"
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    21
  echo "    -q           quiet mode"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    22
  echo
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    23
  echo "  Prepare session directory, including IsaMakefile and document source"
8199
wenzelm
parents: 8198
diff changeset
    24
  echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    25
  echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    26
  exit 1
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    27
}
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    28
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    29
function fail()
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    30
{
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    31
  echo "$1" >&2
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    32
  exit 2
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
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    36
## process command line
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    37
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    38
# options
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    39
8198
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
    40
ISAMAKEFILE="IsaMakefile"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
    41
PARENT=""
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    42
BUILD=""
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    43
QUIET=""
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    44
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    45
while getopts "I:Pbq" OPT
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    46
do
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    47
  case "$OPT" in
8198
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
    48
    I)
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
    49
      ISAMAKEFILE="$OPTARG"
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
    50
      ;;
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
    51
    P)
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
    52
      PARENT=true
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
    53
      ;;
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    54
    b)
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    55
      BUILD=true
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    56
      ;;
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    57
    q)
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    58
      QUIET=true
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    59
      ;;
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    60
    \?)
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    61
      usage
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    62
      ;;
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    63
  esac
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    64
done
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    65
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    66
shift $(($OPTIND - 1))
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    67
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    68
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    69
# args
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    70
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    71
9788
wenzelm
parents: 9656
diff changeset
    72
if [ "$#" -eq 1 ]; then
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
    73
  LOGIC="$ISABELLE_LOGIC"
8685
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    74
  DIR_NAME="$1"; shift
9788
wenzelm
parents: 9656
diff changeset
    75
elif [ "$#" -eq 2 ]; then
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
    76
  LOGIC="$1"; shift
8685
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    77
  DIR_NAME="$1"; shift
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
    78
else
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
    79
  usage
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
    80
fi
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    81
8685
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    82
DIR=$(dirname "$DIR_NAME")
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    83
NAME=$(basename "$DIR_NAME")
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    84
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    85
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    86
## main
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    87
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    88
[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..."
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    89
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
    90
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    91
# IsaMakefile
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
    92
8685
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    93
mkdir -p "$DIR" || fail "Bad directory: $DIR"
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    94
cd "$DIR"
05b6e5bcab66 handle dir prefix;
wenzelm
parents: 8579
diff changeset
    95
8244
c587f5ac4a98 basic source deps;
wenzelm
parents: 8211
diff changeset
    96
DOCUMENT_ROOT=""
11846
2ce611f870e0 option -q also excludes -v true in generated stuff;
wenzelm
parents: 11836
diff changeset
    97
VERBOSE=""
2ce611f870e0 option -q also excludes -v true in generated stuff;
wenzelm
parents: 11836
diff changeset
    98
[ -z "$QUIET" ] && VERBOSE="-v true "
8244
c587f5ac4a98 basic source deps;
wenzelm
parents: 8211
diff changeset
    99
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   100
if [ -n "$BUILD" ]; then
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   101
  IMAGES="$NAME"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   102
  TEST=""
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   103
  TARGET="\$(OUT)/$NAME"
8244
c587f5ac4a98 basic source deps;
wenzelm
parents: 8211
diff changeset
   104
  ROOT_ML="ROOT.ML"
8579
81ef0fc80822 tuned targets;
wenzelm
parents: 8501
diff changeset
   105
  SOURCES="*.thy"
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   106
  DOCUMENT_ROOT="document/root.tex"
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
   107
  USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   108
else
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   109
  IMAGES=""
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   110
  TEST="$NAME"
8211
714f164f0385 rename -p to -P;
wenzelm
parents: 8199
diff changeset
   111
  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
8244
c587f5ac4a98 basic source deps;
wenzelm
parents: 8211
diff changeset
   112
  ROOT_ML="$NAME/ROOT.ML"
8579
81ef0fc80822 tuned targets;
wenzelm
parents: 8501
diff changeset
   113
  SOURCES="$NAME/*.thy"
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   114
  DOCUMENT_ROOT="$NAME/document/root.tex"
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
   115
  USEDIR="\$(USEDIR)"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   116
fi
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   117
8198
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   118
if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   119
  echo "keeping $DIR/$ISAMAKEFILE" >&2
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   120
else
11650
wenzelm
parents: 11578
diff changeset
   121
  [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \
wenzelm
parents: 11578
diff changeset
   122
    echo "creating $DIR/$ISAMAKEFILE" >&2
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   123
  { echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   124
    echo "## targets"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   125
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   126
    echo "default: $NAME"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   127
    echo "images: $IMAGES"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   128
    echo "test: $TEST"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   129
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   130
    echo "all: images test"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   131
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   132
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   133
    echo "## global settings"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   134
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   135
    echo "SRC = \$(ISABELLE_HOME)/src"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   136
    echo "OUT = \$(ISABELLE_OUTPUT)"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   137
    echo "LOG = \$(OUT)/log"
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   138
    echo
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28180
diff changeset
   139
    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   140
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   141
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   142
    echo "## $NAME"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   143
    echo ""
8162
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   144
    if [ -n "$PARENT" ]; then
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   145
      echo "$NAME: $LOGIC $TARGET"
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   146
      echo
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   147
      echo "$LOGIC:"
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28180
diff changeset
   148
      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC"
8162
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   149
      echo
13946
b75562218711 more documentation for packages in root.tex
kleing
parents: 12477
diff changeset
   150
      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
   151
      echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
8162
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   152
    else
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   153
      echo "$NAME: $TARGET"
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   154
      echo
13946
b75562218711 more documentation for packages in root.tex
kleing
parents: 12477
diff changeset
   155
      echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES"
8194
0c5d9d23b715 misc improvements;
wenzelm
parents: 8162
diff changeset
   156
      echo -e "\t@$USEDIR $LOGIC $NAME"
8162
020e384e67dd -p option;
wenzelm
parents: 8159
diff changeset
   157
    fi
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   158
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   159
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   160
    echo "## clean"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   161
    echo
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   162
    echo "clean:"
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   163
    echo -e "\t@rm -f $TARGET"
8198
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   164
  } | {
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   165
    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   166
      cat
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   167
    else
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   168
      cat > "$ISAMAKEFILE"
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   169
    fi
73a5877ca517 -I option;
wenzelm
parents: 8194
diff changeset
   170
  }
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   171
fi
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   172
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   173
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   174
# base directory
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   175
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   176
if [ -z "$BUILD" ]; then
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   177
  mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   178
  cd "$NAME"
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   179
  PREFIX="$DIR/$NAME"
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   180
else
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   181
  PREFIX="$DIR"
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   182
fi
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   183
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   184
if [ -f ROOT.ML ]; then
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   185
  echo "keeping $PREFIX/ROOT.ML" >&2
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   186
else
11650
wenzelm
parents: 11578
diff changeset
   187
  [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   188
  cat >ROOT.ML <<EOF
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   189
(*
32299
5f33ce0ed21f modernized generated example session;
wenzelm
parents: 29143
diff changeset
   190
  no_document use_thys ["This_Theory1", "This_Theory2"];
5f33ce0ed21f modernized generated example session;
wenzelm
parents: 29143
diff changeset
   191
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   192
*)
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   193
EOF
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   194
fi
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   195
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   196
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   197
# document directory
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   198
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   199
if [ -e document ]; then
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   200
  echo "keeping $PREFIX/document" >&2
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   201
else
11650
wenzelm
parents: 11578
diff changeset
   202
  [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   203
  mkdir document || fail "Bad directory: $PREFIX/document"
11650
wenzelm
parents: 11578
diff changeset
   204
wenzelm
parents: 11578
diff changeset
   205
  [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2
16482
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   206
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   207
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   208
  cat >document/root.tex <<EOF
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   209
\documentclass[11pt,a4paper]{article}
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   210
\usepackage{isabelle,isabellesym}
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   211
16482
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   212
% further packages required for unusual symbols (see also
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   213
% isabellesym.sty), use only when needed
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   214
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   215
%\usepackage{amssymb}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   216
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   217
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   218
  %\<triangleq>, \<yen>, \<lozenge>
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   219
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   220
%\usepackage[greek,english]{babel}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   221
  %option greek for \<euro>
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   222
  %option english (default language) for \<guillemotleft>, \<guillemotright>
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   223
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   224
%\usepackage[latin1]{inputenc}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   225
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   226
  %\<threesuperior>, \<threequarters>, \<degree>
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   227
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   228
%\usepackage[only,bigsqcap]{stmaryrd}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   229
  %for \<Sqinter>
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   230
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   231
%\usepackage{eufrak}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   232
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   233
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   234
%\usepackage{textcomp}
ed08c8edc289 be less ambitious about the author's name;
wenzelm
parents: 15920
diff changeset
   235
  %for \<cent>, \<currency>
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   236
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   237
% this should be the last package used
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   238
\usepackage{pdfsetup}
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   239
13946
b75562218711 more documentation for packages in root.tex
kleing
parents: 12477
diff changeset
   240
% urls in roman style, theory text in math-similar italics
10021
6d5d618b302c best-style made default;
wenzelm
parents: 9788
diff changeset
   241
\urlstyle{rm}
6d5d618b302c best-style made default;
wenzelm
parents: 9788
diff changeset
   242
\isabellestyle{it}
9656
a3d868043c49 %\urlstyle{rm}
wenzelm
parents: 9237
diff changeset
   243
28180
3f69c3c54478 added comment
nipkow
parents: 25410
diff changeset
   244
% for uniform font size
3f69c3c54478 added comment
nipkow
parents: 25410
diff changeset
   245
%\renewcommand{\isastyle}{\isastyleminor}
3f69c3c54478 added comment
nipkow
parents: 25410
diff changeset
   246
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   247
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   248
\begin{document}
10353
b1b3f25750f4 tuned tex template;
wenzelm
parents: 10308
diff changeset
   249
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   250
\title{$TITLE}
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   251
\author{$AUTHOR}
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   252
\maketitle
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   253
10308
c50fc8023ac0 make sure default document works;
wenzelm
parents: 10021
diff changeset
   254
\tableofcontents
10353
b1b3f25750f4 tuned tex template;
wenzelm
parents: 10308
diff changeset
   255
25172
ad25033f9ca4 tuned comments;
wenzelm
parents: 24450
diff changeset
   256
% sane default for proof documents
25410
0ba2d51bcb42 reactivated default paragraph formatting for ``proof documents'';
wenzelm
parents: 25172
diff changeset
   257
\parindent 0pt\parskip 0.5ex
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   258
14936
wenzelm
parents: 13948
diff changeset
   259
% generated text of all theories
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   260
\input{session}
10353
b1b3f25750f4 tuned tex template;
wenzelm
parents: 10308
diff changeset
   261
14936
wenzelm
parents: 13948
diff changeset
   262
% optional bibliography
12104
c058fd42b5fc \bibliographystyle{abbrv};
wenzelm
parents: 11878
diff changeset
   263
%\bibliographystyle{abbrv}
10353
b1b3f25750f4 tuned tex template;
wenzelm
parents: 10308
diff changeset
   264
%\bibliography{root}
b1b3f25750f4 tuned tex template;
wenzelm
parents: 10308
diff changeset
   265
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   266
\end{document}
14936
wenzelm
parents: 13948
diff changeset
   267
wenzelm
parents: 13948
diff changeset
   268
%%% Local Variables:
wenzelm
parents: 13948
diff changeset
   269
%%% mode: latex
wenzelm
parents: 13948
diff changeset
   270
%%% TeX-master: t
wenzelm
parents: 13948
diff changeset
   271
%%% End:
8159
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   272
EOF
64c272504383 mkdir: prepare logic session directory;
wenzelm
parents:
diff changeset
   273
fi
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   274
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   275
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   276
# notes
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   277
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   278
if [ -z "$QUIET" ]; then
11650
wenzelm
parents: 11578
diff changeset
   279
  cat >&2 <<EOF
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   280
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   281
Notes:
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   282
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28500
diff changeset
   283
  * 'isabelle make' processes the session (including document preparation)
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   284
11650
wenzelm
parents: 11578
diff changeset
   285
  * $DIR/IsaMakefile contains compilation options and file dependencies
wenzelm
parents: 11578
diff changeset
   286
11846
2ce611f870e0 option -q also excludes -v true in generated stuff;
wenzelm
parents: 11836
diff changeset
   287
  * $PREFIX/document/root.tex contains the LaTeX master document setup
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   288
11846
2ce611f870e0 option -q also excludes -v true in generated stuff;
wenzelm
parents: 11836
diff changeset
   289
  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
11578
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   290
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   291
EOF
43c6735080b8 removed option -d (now standard behaviour);
wenzelm
parents: 10576
diff changeset
   292
fi