1.1 --- a/lib/Tools/latex	Sat Jun 12 13:50:55 2004 +0200
     1.2 +++ b/lib/Tools/latex	Sat Jun 12 22:44:58 2004 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     1.7 -  echo "                 pdf, bbl, png, sty"
     1.8 +  echo "                 pdf, bbl, png, sty, syms"
     1.9    echo
    1.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    1.11    echo "  producing the specified output format."
    1.12 @@ -73,6 +73,9 @@
    1.13  
    1.14  # operations
    1.15  
    1.16 +#set by configure
    1.17 +AUTO_PERL=perl
    1.18 +
    1.19  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    1.20  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    1.21  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    1.22 @@ -81,6 +84,16 @@
    1.23  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.24  function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    1.25  
    1.26 +function extract_syms ()
    1.27 +{
    1.28 +  "$AUTO_PERL" -n \
    1.29 +    -e '!m,%requires, && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    1.30 +    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
    1.31 +  "$AUTO_PERL" -n \
    1.32 +    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    1.33 +    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
    1.34 +}
    1.35 +
    1.36  case "$OUTFORMAT" in
    1.37    dvi)
    1.38      check_root && \
    1.39 @@ -130,6 +143,10 @@
    1.40      copy_styles
    1.41      RC="$?"
    1.42      ;;
    1.43 +  syms)
    1.44 +    extract_syms
    1.45 +    RC="$?"
    1.46 +    ;;
    1.47    *)
    1.48      fail "Bad output format '$OUTFORMAT'"
    1.49      ;;