lib/Tools/mkroot
changeset 48682 162579d4ba15
child 48683 eeb4480b5877
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/mkroot	Sun Aug 05 16:20:34 2012 +0200
     1.3 @@ -0,0 +1,170 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Author: Makarius
     1.7 +#
     1.8 +# DESCRIPTION: prepare session root directory
     1.9 +
    1.10 +
    1.11 +## diagnostics
    1.12 +
    1.13 +PRG="$(basename "$0")"
    1.14 +
    1.15 +function usage()
    1.16 +{
    1.17 +  echo
    1.18 +  echo "Usage: isabelle $PRG NAME"
    1.19 +  echo
    1.20 +  echo "  Prepare session root directory, adding session NAME with"
    1.21 +  echo "  built-in document preparation."
    1.22 +  echo
    1.23 +  exit 1
    1.24 +}
    1.25 +
    1.26 +function fail()
    1.27 +{
    1.28 +  echo "$1" >&2
    1.29 +  exit 2
    1.30 +}
    1.31 +
    1.32 +
    1.33 +## process command line
    1.34 +
    1.35 +[ "$#" -ne 1 -o "$1" = "-?" ] && usage
    1.36 +
    1.37 +DIR_NAME="$1"; shift
    1.38 +
    1.39 +DIR="$(dirname "$DIR_NAME")"
    1.40 +NAME="$(basename "$DIR_NAME")"
    1.41 +
    1.42 +
    1.43 +## main
    1.44 +
    1.45 +[ -e "$DIR_NAME" ] && fail "Cannot overwrite existing \"$DIR_NAME\""
    1.46 +
    1.47 +echo
    1.48 +echo "Preparing session \"$NAME\" ..."
    1.49 +
    1.50 +mkdir -p "$DIR_NAME" || fail "Bad directory: \"$DIR_NAME\""
    1.51 +
    1.52 +
    1.53 +# example theory
    1.54 +
    1.55 +echo "creating $DIR_NAME/Ex.thy"
    1.56 +cat > "$DIR_NAME/Ex.thy" <<EOF
    1.57 +header {* Some example theory *}
    1.58 +
    1.59 +theory Ex imports Main
    1.60 +begin
    1.61 +
    1.62 +text {* Some text here. *}
    1.63 +
    1.64 +end
    1.65 +EOF
    1.66 +
    1.67 +
    1.68 +# document directory
    1.69 +
    1.70 +echo "creating $DIR_NAME/document/root.tex"
    1.71 +
    1.72 +mkdir "$DIR_NAME/document" || fail "Bad directory: \"$DIR_NAME/document\""
    1.73 +
    1.74 +TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
    1.75 +AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
    1.76 +cat > "$DIR_NAME/document/root.tex" <<EOF
    1.77 +\documentclass[11pt,a4paper]{article}
    1.78 +\usepackage{isabelle,isabellesym}
    1.79 +
    1.80 +% further packages required for unusual symbols (see also
    1.81 +% isabellesym.sty), use only when needed
    1.82 +
    1.83 +%\usepackage{amssymb}
    1.84 +  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
    1.85 +  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
    1.86 +  %\<triangleq>, \<yen>, \<lozenge>
    1.87 +
    1.88 +%\usepackage{eurosym}
    1.89 +  %for \<euro>
    1.90 +
    1.91 +%\usepackage[only,bigsqcap]{stmaryrd}
    1.92 +  %for \<Sqinter>
    1.93 +
    1.94 +%\usepackage{eufrak}
    1.95 +  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
    1.96 +
    1.97 +%\usepackage{textcomp}
    1.98 +  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
    1.99 +  %\<currency>
   1.100 +
   1.101 +% this should be the last package used
   1.102 +\usepackage{pdfsetup}
   1.103 +
   1.104 +% urls in roman style, theory text in math-similar italics
   1.105 +\urlstyle{rm}
   1.106 +\isabellestyle{it}
   1.107 +
   1.108 +% for uniform font size
   1.109 +%\renewcommand{\isastyle}{\isastyleminor}
   1.110 +
   1.111 +
   1.112 +\begin{document}
   1.113 +
   1.114 +\title{$TITLE}
   1.115 +\author{$AUTHOR}
   1.116 +\maketitle
   1.117 +
   1.118 +\tableofcontents
   1.119 +
   1.120 +% sane default for proof documents
   1.121 +\parindent 0pt\parskip 0.5ex
   1.122 +
   1.123 +% generated text of all theories
   1.124 +\input{session}
   1.125 +
   1.126 +% optional bibliography
   1.127 +%\bibliographystyle{abbrv}
   1.128 +%\bibliography{root}
   1.129 +
   1.130 +\end{document}
   1.131 +
   1.132 +%%% Local Variables:
   1.133 +%%% mode: latex
   1.134 +%%% TeX-master: t
   1.135 +%%% End:
   1.136 +EOF
   1.137 +
   1.138 +
   1.139 +# ROOT
   1.140 +
   1.141 +if [ -e "$DIR/ROOT" ]; then
   1.142 +  echo "appending to existing ROOT"
   1.143 +  echo >> "$DIR/ROOT"
   1.144 +else
   1.145 +  echo "creating ROOT"
   1.146 +fi
   1.147 +
   1.148 +cat >> "$DIR/ROOT" <<EOF
   1.149 +session "$NAME" = "$ISABELLE_LOGIC" +
   1.150 +  options [document = $ISABELLE_DOC_FORMAT]
   1.151 +  theories "Ex"
   1.152 +  files "document/root.tex"
   1.153 +EOF
   1.154 +
   1.155 +
   1.156 +# notes
   1.157 +
   1.158 +cat <<EOF
   1.159 +
   1.160 +Notes:
   1.161 +
   1.162 +  * $DIR_NAME/Ex.thy contains an example theory
   1.163 +
   1.164 +  * $DIR_NAME/document/root.tex contains the LaTeX master document setup
   1.165 +
   1.166 +  * $DIR/ROOT contains build options, theories and extra file dependencies
   1.167 +
   1.168 +  * the following command line builds the session (with document):
   1.169 +
   1.170 +      isabelle build -v -d $DIR ${ISABELLE_LOGIC}-${NAME}
   1.171 +
   1.172 +EOF
   1.173 +