lib/Tools/latex
changeset 8564 37a1e855390a
parent 7865 d9be8bc5624e
child 8565 3c3895e37761
equal deleted inserted replaced
8563:2746bc9a7ef2 8564:37a1e855390a
    12   echo
    12   echo
    13   echo "Usage: $PRG [OPTIONS] [FILE]"
    13   echo "Usage: $PRG [OPTIONS] [FILE]"
    14   echo
    14   echo
    15   echo "  Options are:"
    15   echo "  Options are:"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    16   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
    17   echo "                 pdf, bbl, png"
    17   echo "                 pdf, bbl, png, sty"
    18   echo
    18   echo
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    19   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    20   echo "  producing the specified output format."
    20   echo "  producing the specified output format."
    21   echo
    21   echo
    22   exit 1
    22   exit 1
    58 [ $# -ne 0 ] && usage
    58 [ $# -ne 0 ] && usage
    59 
    59 
    60 
    60 
    61 ## main
    61 ## main
    62 
    62 
    63 # check file
    63 # root file
    64 
    64 
    65 DIR=$(dirname "$FILE")
    65 DIR=$(dirname "$FILE")
    66 if [ "$DIR" = . ]; then
    66 if [ "$DIR" = . ]; then
    67   FILEBASE=$(basename "$FILE" .tex)
    67   FILEBASE=$(basename "$FILE" .tex)
    68 else
    68 else
    69   FILEBASE=$DIR/$(basename "$FILE" .tex)
    69   FILEBASE=$DIR/$(basename "$FILE" .tex)
    70 fi
    70 fi
    71 
    71 
    72 [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"
    72 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
    73 
    73 
    74 
    74 
    75 # operations
    75 # operations
    76 
    76 
    77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    82 
    82 
    83 
    83 function update_styles ()
    84 # process file
    84 {
       
    85   for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
       
    86   do
       
    87     BNAME=$(basename "$NAME")
       
    88     if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then
       
    89       echo "updating $BNAME"
       
    90       cp -f "$NAME" "$BNAME"
       
    91     fi
       
    92   done
       
    93 }
    85 
    94 
    86 case "$OUTFORMAT" in
    95 case "$OUTFORMAT" in
    87   dvi)
    96   dvi)
       
    97     check_root && \
    88     run_latex
    98     run_latex
    89     RC=$?
    99     RC=$?
    90     ;;
   100     ;;
    91   dvi.gz)
   101   dvi.gz)
       
   102     check_root && \
    92     run_latex && \
   103     run_latex && \
    93     gzip -f "$FILEBASE.dvi"
   104     gzip -f "$FILEBASE.dvi"
    94     RC=$?
   105     RC=$?
    95     ;;
   106     ;;
    96   ps)
   107   ps)
       
   108     check_root && \
    97     run_latex && \
   109     run_latex && \
    98     run_dvips &&
   110     run_dvips &&
    99     RC=$?
   111     RC=$?
   100     ;;
   112     ;;
   101   ps.gz)
   113   ps.gz)
       
   114     check_root && \
   102     run_latex && \
   115     run_latex && \
   103     run_dvips &&
   116     run_dvips &&
   104     gzip -f "$FILEBASE.ps"
   117     gzip -f "$FILEBASE.ps"
   105     RC=$?
   118     RC=$?
   106     ;;
   119     ;;
   107   pdf)
   120   pdf)
       
   121     check_root && \
   108     run_pdflatex
   122     run_pdflatex
   109     RC=$?
   123     RC=$?
   110     ;;
   124     ;;
   111   bbl)
   125   bbl)
       
   126     check_root && \
   112     run_bibtex
   127     run_bibtex
   113     RC=$?
   128     RC=$?
   114     ;;
   129     ;;
   115   png)
   130   png)
       
   131     check_root && \
   116     run_thumbpdf
   132     run_thumbpdf
       
   133     RC=$?
       
   134     ;;
       
   135   sty)
       
   136     update_styles
   117     RC=$?
   137     RC=$?
   118     ;;
   138     ;;
   119   *)
   139   *)
   120     fail "Bad output format '$OUTFORMAT'"
   140     fail "Bad output format '$OUTFORMAT'"
   121     ;;
   141     ;;