# HG changeset patch
# User wenzelm
# Date 1087073098 -7200
# Node ID 4ad751fa50c1e60b8ed377a0bd46188d662279b1
# Parent  a7525235e20fb5770c1da5f7136cd50ca0520f64
added option 'isatool latex -o syms';

diff -r a7525235e20f -r 4ad751fa50c1 doc-src/System/present.tex
--- 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}
 
diff -r a7525235e20f -r 4ad751fa50c1 lib/Tools/latex
--- 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'"
     ;;