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