lib/Tools/document
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
child 32322 45cb4a86eca2
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
     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 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       TAGS="$OPTARG"
    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     IFS=","
    94     for TAG in $TAGS
    95     do
    96       case "$TAG" in
    97         /*)
    98   	  echo "\\isafoldtag{${TAG:1}}"
    99           ;;
   100         -*)
   101   	  echo "\\isadroptag{${TAG:1}}"
   102           ;;
   103         +*)
   104   	  echo "\\isakeeptag{${TAG:1}}"
   105           ;;
   106         *)
   107   	  echo "\\isakeeptag{${TAG}}"
   108           ;;
   109       esac
   110     done
   111   ) > isabelletags.sty
   112 }
   113 
   114 
   115 # prepare document
   116 
   117 function pre_latex ()
   118 {
   119   local FMT="$1"
   120   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
   121   "$ISABELLE_TOOL" latex -o sty && \
   122   "$ISABELLE_TOOL" latex -o "$FMT" && \
   123   { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
   124   { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
   125   "$ISABELLE_TOOL" latex -o "$FMT"
   126 }
   127 
   128 (
   129   cd "$DIR" || fail "Bad directory '$DIR'"
   130 
   131   [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
   132 
   133   prep_tags
   134 
   135   if [ -f IsaMakefile ]; then
   136     "$ISABELLE_TOOL" make "$OUTFORMAT"
   137     RC="$?"
   138   elif [ "$OUTFORMAT" = pdf ]; then
   139     pre_latex pdf && \
   140     "$ISABELLE_TOOL" latex -o pdf
   141     RC="$?"
   142   else
   143     pre_latex dvi && \
   144     "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
   145     RC="$?"
   146   fi
   147 
   148   if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
   149     cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT"
   150   fi
   151 
   152   exit "$RC"
   153 )
   154 RC="$?"
   155 
   156 
   157 # install
   158 
   159 [ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"
   160 
   161 #beware!
   162 [ -n "$CLEAN" ] && rm -rf "$DIR"
   163 
   164 exit "$RC"