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