--- a/doc-src/System/present.tex Sat Jun 12 13:50:55 2004 +0200
+++ b/doc-src/System/present.tex Sat Jun 12 22:44:58 2004 +0200
@@ -553,7 +553,7 @@
Options are:
-o FORMAT specify output format: dvi (default), dvi.gz, ps,
- ps.gz, pdf, bbl, png, sty
+ ps.gz, pdf, bbl, png, sty, syms
Run LaTeX (and related tools) on FILE (default root.tex),
producing the specified output format.
@@ -570,6 +570,9 @@
option \texttt{-D} of the \texttt{usedir} utility, see
\S\ref{sec:tool-usedir}).
+The \texttt{syms} output is for internal use; it generates lists of symbols
+that are available without loading additional {\LaTeX} packages.
+
\subsubsection*{Examples}
--- a/lib/Tools/latex Sat Jun 12 13:50:55 2004 +0200
+++ b/lib/Tools/latex Sat Jun 12 22:44:58 2004 +0200
@@ -16,7 +16,7 @@
echo
echo " Options are:"
echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz,"
- echo " pdf, bbl, png, sty"
+ echo " pdf, bbl, png, sty, syms"
echo
echo " Run LaTeX (and related tools) on FILE (default root.tex),"
echo " producing the specified output format."
@@ -73,6 +73,9 @@
# operations
+#set by configure
+AUTO_PERL=perl
+
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
@@ -81,6 +84,16 @@
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
+function extract_syms ()
+{
+ "$AUTO_PERL" -n \
+ -e '!m,%requires, && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
+ "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
+ "$AUTO_PERL" -n \
+ -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
+ "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
+}
+
case "$OUTFORMAT" in
dvi)
check_root && \
@@ -130,6 +143,10 @@
copy_styles
RC="$?"
;;
+ syms)
+ extract_syms
+ RC="$?"
+ ;;
*)
fail "Bad output format '$OUTFORMAT'"
;;