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