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