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