added option 'isatool latex -o syms';
authorwenzelm
Sat Jun 12 22:44:58 2004 +0200 (2004-06-12)
changeset 149214ad751fa50c1
parent 14920 a7525235e20f
child 14922 88c1e108d0bf
added option 'isatool latex -o syms';
doc-src/System/present.tex
lib/Tools/latex
     1.1 --- a/doc-src/System/present.tex	Sat Jun 12 13:50:55 2004 +0200
     1.2 +++ b/doc-src/System/present.tex	Sat Jun 12 22:44:58 2004 +0200
     1.3 @@ -553,7 +553,7 @@
     1.4  
     1.5    Options are:
     1.6      -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
     1.7 -                 ps.gz, pdf, bbl, png, sty
     1.8 +                 ps.gz, pdf, bbl, png, sty, syms
     1.9  
    1.10    Run LaTeX (and related tools) on FILE (default root.tex),
    1.11    producing the specified output format.
    1.12 @@ -570,6 +570,9 @@
    1.13  option \texttt{-D} of the \texttt{usedir} utility, see
    1.14  \S\ref{sec:tool-usedir}).
    1.15  
    1.16 +The \texttt{syms} output is for internal use; it generates lists of symbols
    1.17 +that are available without loading additional {\LaTeX} packages.
    1.18 +
    1.19  
    1.20  \subsubsection*{Examples}
    1.21  
     2.1 --- a/lib/Tools/latex	Sat Jun 12 13:50:55 2004 +0200
     2.2 +++ b/lib/Tools/latex	Sat Jun 12 22:44:58 2004 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    echo
     2.5    echo "  Options are:"
     2.6    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     2.7 -  echo "                 pdf, bbl, png, sty"
     2.8 +  echo "                 pdf, bbl, png, sty, syms"
     2.9    echo
    2.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    2.11    echo "  producing the specified output format."
    2.12 @@ -73,6 +73,9 @@
    2.13  
    2.14  # operations
    2.15  
    2.16 +#set by configure
    2.17 +AUTO_PERL=perl
    2.18 +
    2.19  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    2.20  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    2.21  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    2.22 @@ -81,6 +84,16 @@
    2.23  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    2.24  function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    2.25  
    2.26 +function extract_syms ()
    2.27 +{
    2.28 +  "$AUTO_PERL" -n \
    2.29 +    -e '!m,%requires, && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
    2.30 +    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
    2.31 +  "$AUTO_PERL" -n \
    2.32 +    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
    2.33 +    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
    2.34 +}
    2.35 +
    2.36  case "$OUTFORMAT" in
    2.37    dvi)
    2.38      check_root && \
    2.39 @@ -130,6 +143,10 @@
    2.40      copy_styles
    2.41      RC="$?"
    2.42      ;;
    2.43 +  syms)
    2.44 +    extract_syms
    2.45 +    RC="$?"
    2.46 +    ;;
    2.47    *)
    2.48      fail "Bad output format '$OUTFORMAT'"
    2.49      ;;