lib/Tools/mkroot
author blanchet
Wed May 21 14:09:42 2014 +0200 (2014-05-21)
changeset 57037 c51132be8e16
parent 56786 13ede133f6eb
child 66948 47249c5ec3a4
permissions -rwxr-xr-x
avoid markup-generating @{make_string}
wenzelm@48682
     1
#!/usr/bin/env bash
wenzelm@48682
     2
#
wenzelm@48682
     3
# Author: Makarius
wenzelm@48682
     4
#
wenzelm@48682
     5
# DESCRIPTION: prepare session root directory
wenzelm@48682
     6
wenzelm@48682
     7
wenzelm@48682
     8
## diagnostics
wenzelm@48682
     9
wenzelm@48682
    10
PRG="$(basename "$0")"
wenzelm@48682
    11
wenzelm@48682
    12
function usage()
wenzelm@48682
    13
{
wenzelm@48682
    14
  echo
wenzelm@48739
    15
  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
wenzelm@48682
    16
  echo
wenzelm@48739
    17
  echo "  Options are:"
wenzelm@48739
    18
  echo "    -d           enable document preparation"
wenzelm@48739
    19
  echo "    -n NAME      alternative session name (default: DIR base name)"
wenzelm@48739
    20
  echo
wenzelm@48739
    21
  echo "  Prepare session root DIR (default: current directory)."
wenzelm@48682
    22
  echo
wenzelm@48682
    23
  exit 1
wenzelm@48682
    24
}
wenzelm@48682
    25
wenzelm@48682
    26
function fail()
wenzelm@48682
    27
{
wenzelm@48682
    28
  echo "$1" >&2
wenzelm@48682
    29
  exit 2
wenzelm@48682
    30
}
wenzelm@48682
    31
wenzelm@48682
    32
wenzelm@48682
    33
## process command line
wenzelm@48682
    34
wenzelm@48739
    35
# options
wenzelm@48739
    36
wenzelm@48739
    37
DOC=""
wenzelm@48739
    38
NAME=""
wenzelm@48682
    39
wenzelm@48739
    40
while getopts "n:d" OPT
wenzelm@48739
    41
do
wenzelm@48739
    42
  case "$OPT" in
wenzelm@48739
    43
    d)
wenzelm@48739
    44
      DOC="true"
wenzelm@48739
    45
      ;;
wenzelm@48739
    46
    n)
wenzelm@48739
    47
      NAME="$OPTARG"
wenzelm@48739
    48
      ;;
wenzelm@48739
    49
    \?)
wenzelm@48739
    50
      usage
wenzelm@48739
    51
      ;;
wenzelm@48739
    52
  esac
wenzelm@48739
    53
done
wenzelm@48682
    54
wenzelm@48739
    55
shift $(($OPTIND - 1))
wenzelm@48739
    56
wenzelm@48739
    57
wenzelm@48739
    58
# args
wenzelm@48739
    59
wenzelm@48739
    60
if [ "$#" -eq 0 ]; then
wenzelm@48739
    61
  DIR="."
wenzelm@48739
    62
elif [ "$#" -eq 1 ]; then
wenzelm@48739
    63
  DIR="$1"
wenzelm@48739
    64
  shift
wenzelm@48739
    65
else
wenzelm@48739
    66
  usage
wenzelm@48739
    67
fi
wenzelm@48682
    68
wenzelm@48682
    69
wenzelm@48682
    70
## main
wenzelm@48682
    71
wenzelm@48739
    72
mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
wenzelm@48739
    73
wenzelm@48739
    74
[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
wenzelm@48739
    75
wenzelm@48739
    76
[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
wenzelm@48739
    77
wenzelm@48739
    78
[ "$DOC" = true -a -e "$DIR/document" ] && \
wenzelm@48739
    79
  fail "Cannot overwrite existing $DIR/document"
wenzelm@48682
    80
wenzelm@48682
    81
echo
wenzelm@48739
    82
echo "Preparing session \"$NAME\" in \"$DIR\""
wenzelm@48682
    83
wenzelm@48682
    84
wenzelm@48739
    85
# ROOT
wenzelm@48682
    86
wenzelm@48739
    87
echo "  creating $DIR/ROOT"
wenzelm@48682
    88
wenzelm@48739
    89
if [ "$DOC" = true ]; then
wenzelm@48739
    90
  cat > "$DIR/ROOT" <<EOF
wenzelm@48739
    91
session "$NAME" = "$ISABELLE_LOGIC" +
wenzelm@52743
    92
  options [document = pdf, document_output = "output"]
wenzelm@48739
    93
  theories [document = false]
wenzelm@56786
    94
    (* Foo *)
wenzelm@56786
    95
    (* Bar *)
wenzelm@48739
    96
  theories
wenzelm@48739
    97
    (* Baz *)
wenzelm@56786
    98
  document_files
wenzelm@56786
    99
    "root.tex"
wenzelm@48682
   100
EOF
wenzelm@48739
   101
else
wenzelm@48739
   102
  cat > "$DIR/ROOT" <<EOF
wenzelm@48739
   103
session "$NAME" = "$ISABELLE_LOGIC" +
wenzelm@48739
   104
  options [document = false]
wenzelm@48739
   105
  theories
wenzelm@56786
   106
    (* Foo *)
wenzelm@56786
   107
    (* Bar *)
wenzelm@56786
   108
    (* Baz *)
wenzelm@48739
   109
EOF
wenzelm@48739
   110
fi
wenzelm@48682
   111
wenzelm@48682
   112
wenzelm@48682
   113
# document directory
wenzelm@48682
   114
wenzelm@48739
   115
if [ "$DOC" = true ]; then
wenzelm@48739
   116
  echo "  creating $DIR/document/root.tex"
wenzelm@48682
   117
wenzelm@48739
   118
  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
wenzelm@48739
   119
  
wenzelm@48739
   120
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
wenzelm@48739
   121
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
wenzelm@48739
   122
wenzelm@48739
   123
  cat > "$DIR/document/root.tex" <<EOF
wenzelm@48682
   124
\documentclass[11pt,a4paper]{article}
wenzelm@48682
   125
\usepackage{isabelle,isabellesym}
wenzelm@48682
   126
wenzelm@48682
   127
% further packages required for unusual symbols (see also
wenzelm@48682
   128
% isabellesym.sty), use only when needed
wenzelm@48682
   129
wenzelm@48682
   130
%\usepackage{amssymb}
wenzelm@48682
   131
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
wenzelm@48682
   132
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
wenzelm@48682
   133
  %\<triangleq>, \<yen>, \<lozenge>
wenzelm@48682
   134
wenzelm@48682
   135
%\usepackage{eurosym}
wenzelm@48682
   136
  %for \<euro>
wenzelm@48682
   137
wenzelm@48682
   138
%\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@48682
   139
  %for \<Sqinter>
wenzelm@48682
   140
wenzelm@48682
   141
%\usepackage{eufrak}
wenzelm@48682
   142
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
wenzelm@48682
   143
wenzelm@48682
   144
%\usepackage{textcomp}
wenzelm@48682
   145
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
wenzelm@48682
   146
  %\<currency>
wenzelm@48682
   147
wenzelm@48682
   148
% this should be the last package used
wenzelm@48682
   149
\usepackage{pdfsetup}
wenzelm@48682
   150
wenzelm@48682
   151
% urls in roman style, theory text in math-similar italics
wenzelm@48682
   152
\urlstyle{rm}
wenzelm@48682
   153
\isabellestyle{it}
wenzelm@48682
   154
wenzelm@48682
   155
% for uniform font size
wenzelm@48682
   156
%\renewcommand{\isastyle}{\isastyleminor}
wenzelm@48682
   157
wenzelm@48682
   158
wenzelm@48682
   159
\begin{document}
wenzelm@48682
   160
wenzelm@48682
   161
\title{$TITLE}
wenzelm@48682
   162
\author{$AUTHOR}
wenzelm@48682
   163
\maketitle
wenzelm@48682
   164
wenzelm@48682
   165
\tableofcontents
wenzelm@48682
   166
wenzelm@48682
   167
% sane default for proof documents
wenzelm@48682
   168
\parindent 0pt\parskip 0.5ex
wenzelm@48682
   169
wenzelm@48682
   170
% generated text of all theories
wenzelm@48682
   171
\input{session}
wenzelm@48682
   172
wenzelm@48682
   173
% optional bibliography
wenzelm@48682
   174
%\bibliographystyle{abbrv}
wenzelm@48682
   175
%\bibliography{root}
wenzelm@48682
   176
wenzelm@48682
   177
\end{document}
wenzelm@48682
   178
wenzelm@48682
   179
%%% Local Variables:
wenzelm@48682
   180
%%% mode: latex
wenzelm@48682
   181
%%% TeX-master: t
wenzelm@48682
   182
%%% End:
wenzelm@48682
   183
EOF
wenzelm@48682
   184
fi
wenzelm@48682
   185
wenzelm@48682
   186
# notes
wenzelm@48682
   187
wenzelm@48739
   188
declare -a DIR_PARTS=($DIR)
wenzelm@48739
   189
if [ ${#DIR_PARTS[@]} = 1 ]; then
wenzelm@48739
   190
  OPT_DIR="-D $DIR"
wenzelm@48683
   191
else
wenzelm@48739
   192
  OPT_DIR="-D \"$DIR\""
wenzelm@48683
   193
fi
wenzelm@48683
   194
wenzelm@48682
   195
cat <<EOF
wenzelm@48682
   196
wenzelm@48739
   197
Now use the following command line to build the session:
wenzelm@48682
   198
wenzelm@48805
   199
  isabelle build $OPT_DIR
wenzelm@48682
   200
wenzelm@48682
   201
EOF
wenzelm@48682
   202