# HG changeset patch
# User wenzelm
# Date 981312090 -3600
# Node ID 1379e49c0ee961250a670c4d2a256d1c9560521a
# Parent  00b70f3196c2b746a6ba06fa67e01fe79b685fea
added no_document;

diff -r 00b70f3196c2 -r 1379e49c0ee9 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Sun Feb 04 19:40:54 2001 +0100
+++ b/doc-src/Ref/theories.tex	Sun Feb 04 19:41:30 2001 +0100
@@ -291,6 +291,7 @@
 del_path: string -> unit
 reset_path: unit -> unit
 with_path: string -> ('a -> 'b) -> 'a -> 'b
+no_document: ('a -> 'b) -> 'a -> 'b
 \end{ttbox}
 
 \begin{ttdescription}
@@ -307,7 +308,10 @@
   (current directory) only.
   
 \item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
-  $dir$ to the beginning of the load path before executing $(f~x)$.
+  $dir$ to the beginning of the load path while executing $(f~x)$.
+  
+\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
+  document generation while executing $(f~x)$.
 
 \end{ttdescription}