lib/Tools/document
author wenzelm
Thu Apr 24 00:29:55 2014 +0200 (2014-04-24)
changeset 56686 2386d1a3ca8f
parent 52748 8e398d9bedf3
child 62589 b5783412bfed
permissions -rwxr-xr-x
canonical list operations, as in ML;
avoid odd mutable data structures;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # DESCRIPTION: prepare theory session document
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage()
    11 {
    12   echo
    13   echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    14   echo
    15   echo "  Options are:"
    16   echo "    -c           cleanup -- be aggressive in removing old stuff"
    17   echo "    -n NAME      specify document name (default 'document')"
    18   echo "    -o FORMAT    specify output format: pdf (default), dvi"
    19   echo "    -t TAGS      specify tagged region markup"
    20   echo
    21   echo "  Prepare the theory session document in DIR (default 'document')"
    22   echo "  producing the specified output format."
    23   echo
    24   exit 1
    25 }
    26 
    27 function fail()
    28 {
    29   echo "$1" >&2
    30   exit 2
    31 }
    32 
    33 
    34 ## process command line
    35 
    36 # options
    37 
    38 CLEAN=""
    39 NAME="document"
    40 OUTFORMAT=pdf
    41 declare -a TAGS=()
    42 
    43 while getopts "cn:o:t:" OPT
    44 do
    45   case "$OPT" in
    46     c)
    47       CLEAN=true
    48       ;;
    49     n)
    50       NAME="$OPTARG"
    51       ;;
    52     o)
    53       OUTFORMAT="$OPTARG"
    54       ;;
    55     t)
    56       splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
    57       ;;
    58     \?)
    59       usage
    60       ;;
    61   esac
    62 done
    63 
    64 shift $(($OPTIND - 1))
    65 
    66 
    67 # args
    68 
    69 DIR="document"
    70 [ "$#" -ge 1 ] && { DIR="$1"; shift; }
    71 
    72 [ "$#" -ne 0 ] && usage
    73 
    74 
    75 ## main
    76 
    77 # check format
    78 
    79 case "$OUTFORMAT" in
    80   pdf | dvi)
    81     ;;
    82   *)
    83     fail "Bad output format '$OUTFORMAT'"
    84     ;;
    85 esac
    86 
    87 
    88 # document variants
    89 
    90 ROOT_NAME="root_$NAME"
    91 [ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
    92 
    93 function prep_tags ()
    94 {
    95   (
    96     for TAG in "${TAGS[@]}"
    97     do
    98       case "$TAG" in
    99         /*)
   100           echo "\\isafoldtag{${TAG:1}}"
   101           ;;
   102         -*)
   103           echo "\\isadroptag{${TAG:1}}"
   104           ;;
   105         +*)
   106           echo "\\isakeeptag{${TAG:1}}"
   107           ;;
   108         *)
   109           echo "\\isakeeptag{${TAG}}"
   110           ;;
   111       esac
   112     done
   113     echo
   114   ) > isabelletags.sty
   115 }
   116 
   117 
   118 # prepare document
   119 
   120 (
   121   cd "$DIR" || fail "Bad directory '$DIR'"
   122 
   123   [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   124 
   125   prep_tags
   126 
   127   if [ -f build ]; then
   128     ./build "$OUTFORMAT" "$NAME"
   129     RC="$?"
   130   else
   131     "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
   132     "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   133     { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
   134     { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
   135     "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
   136     "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
   137     RC="$?"
   138   fi
   139 
   140   if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
   141     cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   142   fi
   143 
   144   exit "$RC"
   145 )
   146 RC="$?"
   147 
   148 
   149 # install
   150 
   151 [ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
   152 
   153 #beware!
   154 [ -n "$CLEAN" ] && rm -rf "$DIR"
   155 
   156 exit "$RC"