lib/Tools/document
author wenzelm
Tue Aug 04 15:05:34 2009 +0200 (2009-08-04)
changeset 32322 45cb4a86eca2
parent 29143 72c960b2b83e
child 32390 468eff174a77
permissions -rwxr-xr-x
change IFS only locally -- thanks to bash arrays;
     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: dvi (default), dvi.gz, ps, ps.gz, pdf"
    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=dvi
    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       ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
    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   dvi | dvi.gz | ps | ps.gz | pdf)
    81     ;;
    82   *)
    83     fail "Bad output format '$OUTFORMAT'"
    84     ;;
    85 esac
    86 
    87 
    88 # tagged region markup
    89 
    90 function prep_tags ()
    91 {
    92   (
    93     for TAG in "${TAGS[@]}"
    94     do
    95       case "$TAG" in
    96         /*)
    97           echo "\\isafoldtag{${TAG:1}}"
    98           ;;
    99         -*)
   100           echo "\\isadroptag{${TAG:1}}"
   101           ;;
   102         +*)
   103           echo "\\isakeeptag{${TAG:1}}"
   104           ;;
   105         *)
   106           echo "\\isakeeptag{${TAG}}"
   107           ;;
   108       esac
   109     done
   110   ) > isabelletags.sty
   111 }
   112 
   113 
   114 # prepare document
   115 
   116 function pre_latex ()
   117 {
   118   local FMT="$1"
   119   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   120   "$ISABELLE_TOOL" latex -o sty && \
   121   "$ISABELLE_TOOL" latex -o "$FMT" && \
   122   { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
   123   { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
   124   "$ISABELLE_TOOL" latex -o "$FMT"
   125 }
   126 
   127 (
   128   cd "$DIR" || fail "Bad directory '$DIR'"
   129 
   130   [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
   131 
   132   prep_tags
   133 
   134   if [ -f IsaMakefile ]; then
   135     "$ISABELLE_TOOL" make "$OUTFORMAT"
   136     RC="$?"
   137   elif [ "$OUTFORMAT" = pdf ]; then
   138     pre_latex pdf && \
   139     "$ISABELLE_TOOL" latex -o pdf
   140     RC="$?"
   141   else
   142     pre_latex dvi && \
   143     "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
   144     RC="$?"
   145   fi
   146 
   147   if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
   148     cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   149   fi
   150 
   151   exit "$RC"
   152 )
   153 RC="$?"
   154 
   155 
   156 # install
   157 
   158 [ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
   159 
   160 #beware!
   161 [ -n "$CLEAN" ] && rm -rf "$DIR"
   162 
   163 exit "$RC"