lib/Tools/mkroot
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 66948 47249c5ec3a4
permissions -rwxr-xr-x
more robust sorted_entries;
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
  theories
wenzelm@56786
   105
    (* Foo *)
wenzelm@56786
   106
    (* Bar *)
wenzelm@56786
   107
    (* Baz *)
wenzelm@48739
   108
EOF
wenzelm@48739
   109
fi
wenzelm@48682
   110
wenzelm@48682
   111
wenzelm@48682
   112
# document directory
wenzelm@48682
   113
wenzelm@48739
   114
if [ "$DOC" = true ]; then
wenzelm@48739
   115
  echo "  creating $DIR/document/root.tex"
wenzelm@48682
   116
wenzelm@48739
   117
  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
wenzelm@48739
   118
  
wenzelm@48739
   119
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
wenzelm@48739
   120
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
wenzelm@48739
   121
wenzelm@48739
   122
  cat > "$DIR/document/root.tex" <<EOF
wenzelm@48682
   123
\documentclass[11pt,a4paper]{article}
wenzelm@48682
   124
\usepackage{isabelle,isabellesym}
wenzelm@48682
   125
wenzelm@48682
   126
% further packages required for unusual symbols (see also
wenzelm@48682
   127
% isabellesym.sty), use only when needed
wenzelm@48682
   128
wenzelm@48682
   129
%\usepackage{amssymb}
wenzelm@48682
   130
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
wenzelm@48682
   131
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
wenzelm@48682
   132
  %\<triangleq>, \<yen>, \<lozenge>
wenzelm@48682
   133
wenzelm@48682
   134
%\usepackage{eurosym}
wenzelm@48682
   135
  %for \<euro>
wenzelm@48682
   136
wenzelm@48682
   137
%\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@48682
   138
  %for \<Sqinter>
wenzelm@48682
   139
wenzelm@48682
   140
%\usepackage{eufrak}
wenzelm@48682
   141
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
wenzelm@48682
   142
wenzelm@48682
   143
%\usepackage{textcomp}
wenzelm@48682
   144
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
wenzelm@48682
   145
  %\<currency>
wenzelm@48682
   146
wenzelm@48682
   147
% this should be the last package used
wenzelm@48682
   148
\usepackage{pdfsetup}
wenzelm@48682
   149
wenzelm@48682
   150
% urls in roman style, theory text in math-similar italics
wenzelm@48682
   151
\urlstyle{rm}
wenzelm@48682
   152
\isabellestyle{it}
wenzelm@48682
   153
wenzelm@48682
   154
% for uniform font size
wenzelm@48682
   155
%\renewcommand{\isastyle}{\isastyleminor}
wenzelm@48682
   156
wenzelm@48682
   157
wenzelm@48682
   158
\begin{document}
wenzelm@48682
   159
wenzelm@48682
   160
\title{$TITLE}
wenzelm@48682
   161
\author{$AUTHOR}
wenzelm@48682
   162
\maketitle
wenzelm@48682
   163
wenzelm@48682
   164
\tableofcontents
wenzelm@48682
   165
wenzelm@48682
   166
% sane default for proof documents
wenzelm@48682
   167
\parindent 0pt\parskip 0.5ex
wenzelm@48682
   168
wenzelm@48682
   169
% generated text of all theories
wenzelm@48682
   170
\input{session}
wenzelm@48682
   171
wenzelm@48682
   172
% optional bibliography
wenzelm@48682
   173
%\bibliographystyle{abbrv}
wenzelm@48682
   174
%\bibliography{root}
wenzelm@48682
   175
wenzelm@48682
   176
\end{document}
wenzelm@48682
   177
wenzelm@48682
   178
%%% Local Variables:
wenzelm@48682
   179
%%% mode: latex
wenzelm@48682
   180
%%% TeX-master: t
wenzelm@48682
   181
%%% End:
wenzelm@48682
   182
EOF
wenzelm@48682
   183
fi
wenzelm@48682
   184
wenzelm@48682
   185
# notes
wenzelm@48682
   186
wenzelm@48739
   187
declare -a DIR_PARTS=($DIR)
wenzelm@48739
   188
if [ ${#DIR_PARTS[@]} = 1 ]; then
wenzelm@48739
   189
  OPT_DIR="-D $DIR"
wenzelm@48683
   190
else
wenzelm@48739
   191
  OPT_DIR="-D \"$DIR\""
wenzelm@48683
   192
fi
wenzelm@48683
   193
wenzelm@48682
   194
cat <<EOF
wenzelm@48682
   195
wenzelm@48739
   196
Now use the following command line to build the session:
wenzelm@48682
   197
wenzelm@48805
   198
  isabelle build $OPT_DIR
wenzelm@48682
   199
wenzelm@48682
   200
EOF
wenzelm@48682
   201