lib/Tools/mkroot
author wenzelm
Sun Aug 05 20:11:32 2012 +0200 (2012-08-05)
changeset 48683 eeb4480b5877
parent 48682 162579d4ba15
child 48739 3a6c03b15916
permissions -rwxr-xr-x
more on isabelle mkroot;
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@48682
    15
  echo "Usage: isabelle $PRG NAME"
wenzelm@48682
    16
  echo
wenzelm@48682
    17
  echo "  Prepare session root directory, adding session NAME with"
wenzelm@48682
    18
  echo "  built-in document preparation."
wenzelm@48682
    19
  echo
wenzelm@48682
    20
  exit 1
wenzelm@48682
    21
}
wenzelm@48682
    22
wenzelm@48682
    23
function fail()
wenzelm@48682
    24
{
wenzelm@48682
    25
  echo "$1" >&2
wenzelm@48682
    26
  exit 2
wenzelm@48682
    27
}
wenzelm@48682
    28
wenzelm@48682
    29
wenzelm@48682
    30
## process command line
wenzelm@48682
    31
wenzelm@48682
    32
[ "$#" -ne 1 -o "$1" = "-?" ] && usage
wenzelm@48682
    33
wenzelm@48682
    34
DIR_NAME="$1"; shift
wenzelm@48682
    35
wenzelm@48682
    36
DIR="$(dirname "$DIR_NAME")"
wenzelm@48682
    37
NAME="$(basename "$DIR_NAME")"
wenzelm@48682
    38
wenzelm@48682
    39
wenzelm@48682
    40
## main
wenzelm@48682
    41
wenzelm@48682
    42
[ -e "$DIR_NAME" ] && fail "Cannot overwrite existing \"$DIR_NAME\""
wenzelm@48682
    43
wenzelm@48682
    44
echo
wenzelm@48682
    45
echo "Preparing session \"$NAME\" ..."
wenzelm@48682
    46
wenzelm@48682
    47
mkdir -p "$DIR_NAME" || fail "Bad directory: \"$DIR_NAME\""
wenzelm@48682
    48
wenzelm@48682
    49
wenzelm@48682
    50
# example theory
wenzelm@48682
    51
wenzelm@48682
    52
echo "creating $DIR_NAME/Ex.thy"
wenzelm@48682
    53
cat > "$DIR_NAME/Ex.thy" <<EOF
wenzelm@48682
    54
header {* Some example theory *}
wenzelm@48682
    55
wenzelm@48682
    56
theory Ex imports Main
wenzelm@48682
    57
begin
wenzelm@48682
    58
wenzelm@48682
    59
text {* Some text here. *}
wenzelm@48682
    60
wenzelm@48682
    61
end
wenzelm@48682
    62
EOF
wenzelm@48682
    63
wenzelm@48682
    64
wenzelm@48682
    65
# document directory
wenzelm@48682
    66
wenzelm@48682
    67
echo "creating $DIR_NAME/document/root.tex"
wenzelm@48682
    68
wenzelm@48682
    69
mkdir "$DIR_NAME/document" || fail "Bad directory: \"$DIR_NAME/document\""
wenzelm@48682
    70
wenzelm@48682
    71
TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
wenzelm@48682
    72
AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
wenzelm@48682
    73
cat > "$DIR_NAME/document/root.tex" <<EOF
wenzelm@48682
    74
\documentclass[11pt,a4paper]{article}
wenzelm@48682
    75
\usepackage{isabelle,isabellesym}
wenzelm@48682
    76
wenzelm@48682
    77
% further packages required for unusual symbols (see also
wenzelm@48682
    78
% isabellesym.sty), use only when needed
wenzelm@48682
    79
wenzelm@48682
    80
%\usepackage{amssymb}
wenzelm@48682
    81
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
wenzelm@48682
    82
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
wenzelm@48682
    83
  %\<triangleq>, \<yen>, \<lozenge>
wenzelm@48682
    84
wenzelm@48682
    85
%\usepackage{eurosym}
wenzelm@48682
    86
  %for \<euro>
wenzelm@48682
    87
wenzelm@48682
    88
%\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@48682
    89
  %for \<Sqinter>
wenzelm@48682
    90
wenzelm@48682
    91
%\usepackage{eufrak}
wenzelm@48682
    92
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
wenzelm@48682
    93
wenzelm@48682
    94
%\usepackage{textcomp}
wenzelm@48682
    95
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
wenzelm@48682
    96
  %\<currency>
wenzelm@48682
    97
wenzelm@48682
    98
% this should be the last package used
wenzelm@48682
    99
\usepackage{pdfsetup}
wenzelm@48682
   100
wenzelm@48682
   101
% urls in roman style, theory text in math-similar italics
wenzelm@48682
   102
\urlstyle{rm}
wenzelm@48682
   103
\isabellestyle{it}
wenzelm@48682
   104
wenzelm@48682
   105
% for uniform font size
wenzelm@48682
   106
%\renewcommand{\isastyle}{\isastyleminor}
wenzelm@48682
   107
wenzelm@48682
   108
wenzelm@48682
   109
\begin{document}
wenzelm@48682
   110
wenzelm@48682
   111
\title{$TITLE}
wenzelm@48682
   112
\author{$AUTHOR}
wenzelm@48682
   113
\maketitle
wenzelm@48682
   114
wenzelm@48682
   115
\tableofcontents
wenzelm@48682
   116
wenzelm@48682
   117
% sane default for proof documents
wenzelm@48682
   118
\parindent 0pt\parskip 0.5ex
wenzelm@48682
   119
wenzelm@48682
   120
% generated text of all theories
wenzelm@48682
   121
\input{session}
wenzelm@48682
   122
wenzelm@48682
   123
% optional bibliography
wenzelm@48682
   124
%\bibliographystyle{abbrv}
wenzelm@48682
   125
%\bibliography{root}
wenzelm@48682
   126
wenzelm@48682
   127
\end{document}
wenzelm@48682
   128
wenzelm@48682
   129
%%% Local Variables:
wenzelm@48682
   130
%%% mode: latex
wenzelm@48682
   131
%%% TeX-master: t
wenzelm@48682
   132
%%% End:
wenzelm@48682
   133
EOF
wenzelm@48682
   134
wenzelm@48682
   135
wenzelm@48682
   136
# ROOT
wenzelm@48682
   137
wenzelm@48682
   138
if [ -e "$DIR/ROOT" ]; then
wenzelm@48682
   139
  echo "appending to existing ROOT"
wenzelm@48682
   140
  echo >> "$DIR/ROOT"
wenzelm@48682
   141
else
wenzelm@48682
   142
  echo "creating ROOT"
wenzelm@48682
   143
fi
wenzelm@48682
   144
wenzelm@48682
   145
cat >> "$DIR/ROOT" <<EOF
wenzelm@48683
   146
session "$NAME"! = "$ISABELLE_LOGIC" +
wenzelm@48682
   147
  options [document = $ISABELLE_DOC_FORMAT]
wenzelm@48682
   148
  theories "Ex"
wenzelm@48682
   149
  files "document/root.tex"
wenzelm@48682
   150
EOF
wenzelm@48682
   151
wenzelm@48682
   152
wenzelm@48682
   153
# notes
wenzelm@48682
   154
wenzelm@48683
   155
if [ "$DIR" = . ]; then
wenzelm@48683
   156
  OPT_DIR="-d."
wenzelm@48683
   157
else
wenzelm@48683
   158
  OPT_DIR="-d \"$DIR\""
wenzelm@48683
   159
fi
wenzelm@48683
   160
wenzelm@48682
   161
cat <<EOF
wenzelm@48682
   162
wenzelm@48682
   163
Notes:
wenzelm@48682
   164
wenzelm@48683
   165
  * $DIR_NAME/Ex.thy contains an example theory.
wenzelm@48682
   166
wenzelm@48683
   167
  * $DIR_NAME/document/root.tex contains the LaTeX master document setup.
wenzelm@48682
   168
wenzelm@48683
   169
  * $DIR/ROOT contains build options, theories and extra file dependencies.
wenzelm@48682
   170
wenzelm@48683
   171
  * The following command line builds the session (with document):
wenzelm@48682
   172
wenzelm@48683
   173
      isabelle build -v $OPT_DIR $NAME
wenzelm@48682
   174
wenzelm@48682
   175
EOF
wenzelm@48682
   176