# HG changeset patch
# User clasohm
# Date 754219780 -3600
# Node ID a133921366cb7611d72b7ec20ede3b4e76f0c6f9
# Parent  3a8c68d1d46615bc1a21559ab628bab35b35fc1b
added index commands, removed last paragraph of "Using Poly/ML"

diff -r 3a8c68d1d466 -r a133921366cb doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Tue Nov 23 10:47:33 1993 +0100
+++ b/doc-src/Ref/introduction.tex	Thu Nov 25 10:29:40 1993 +0100
@@ -94,9 +94,7 @@
 time_use        : string -> unit
 time_use_thy    : string -> unit
 update          : unit -> unit
-unlink_thy      : string -> unit
 loadpath        : string list ref
-delete_tmpfiles : bool ref
 \end{ttbox}
 \begin{description}
 \item[\ttindexbold{cd} \tt"{\it dir}";]  changes to {\it dir\/} the default
@@ -123,18 +121,9 @@
 reads all theories that have changed since the last time they have been read.
 See Chapter~\ref{theories} for details.
 
-\item[\ttindexbold{unlink_thy} \tt"$tname$";]  
-removes theory {\it tname} from internal list of theory dependencies and has to
-be used after removing a theory's files. Else {\tt update} would keep on
-searching for them. See Chapter~\ref{theories} for details.
-
 \item[\ttindexbold{loadpath}] contains a list of paths that is used by 
 {\tt use_thy} and {\tt update} to find {\it tname}{\tt.ML} and {\it tname}
 {\tt.thy}. See Chapter~\ref{theories} for details.
-
-\item[\ttindexbold{delete_tmpfiles}] is used by use_thy and controls the
-removal of temporary files created during the reading of {\it tname}{\tt.thy}.
-See Chapter~\ref{theories} for details.
 \end{description}
 
 
diff -r 3a8c68d1d466 -r a133921366cb doc-src/Ref/ref.toc
--- a/doc-src/Ref/ref.toc	Tue Nov 23 10:47:33 1993 +0100
+++ b/doc-src/Ref/ref.toc	Thu Nov 25 10:29:40 1993 +0100
@@ -5,7 +5,7 @@
 \contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3}
 \contentsline {subsection}{Printing limits}{3}
 \contentsline {subsection}{Printing of meta-level hypotheses}{3}
-\contentsline {subsection}{Printing of types and sorts}{4}
+\contentsline {subsection}{Printing of types and sorts}{3}
 \contentsline {subsection}{$\eta $-contraction before printing}{4}
 \contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
 \contentsline {section}{\numberline {1.6}Shell scripts}{5}
diff -r 3a8c68d1d466 -r a133921366cb doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Tue Nov 23 10:47:33 1993 +0100
+++ b/doc-src/Ref/theories.tex	Thu Nov 25 10:29:40 1993 +0100
@@ -157,12 +157,13 @@
 
 
 \subsection{Filenames and paths}
+\indexbold{filenames}
 
 The files the theory definition resides in must have the lower case name of
-the theory with ".thy" or ".ML" appended.  On the other hand {\tt use_thy}'s
+the theory with ".thy" or ".ML" appended.  On the other hand \ttindex{use_thy}'s
 parameter has to be the exact theory name.  Optionally the name can be
 preceeded by a path to specify the directory where the files can be found.  If
-no path is provided the reference variable {\tt loadpath} is used which
+no path is provided the reference variable \ttindexbold{loadpath} is used which
 contains a list of paths that are searched in the given order.  After the
 ".thy"-file for a theory has been found, the same path is used to locate the
 (optional) ".ML"-file.  (You might note that it is also possible to only
@@ -173,33 +174,34 @@
 
 
 \subsection{Reloading a theory}
+\index{reloading a theory}
 
-{\tt use_thy} keeps track of all loaded theories and stores information about
-their files.  If it finds that the theory to be loaded was already read
+\ttindex{use_thy} keeps track of all loaded theories and stores information
+about their files.  If it finds that the theory to be loaded was already read
 before, the following happens: First the theory's files are searched at the
-place they were located the last time they were read. If they are found,
-their time of last modification is compared to the internal data and {\tt
-  use_thy} stops if they are equal. In case the files have been moved, {\tt
-  use_thy} searches them the same way a new theory would be searched for.
-After all these tests have been passed, the theory is reloaded and all
-theories that depend on it (i.e. that have its name in their $theoryDef$) are
-marked as out-of-date.
+place they were located the last time they were read. If they are found, their
+time of last modification is compared to the internal data and {\tt use_thy}
+stops if they are equal. In case the files have been moved, {\tt use_thy}
+searches them the same way a new theory would be searched for.  After all these
+tests have been passed, the theory is reloaded and all theories that depend on
+it (i.e. that have its name in their $theoryDef$) are marked as out-of-date.
 
 As changing a theory often makes it necessary to reload all theories that
-(indirectly) depend on it, {\tt update} should be used instead of {\tt
+(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt
 use_thy} to read a modified theory.  This function reloads all changed
 theories and their descendants in the correct order.
 
 
 \subsection{Pseudo theories}
+\indexbold{pseudo theories}
 
-There is a problem with {\tt update}: objects created in \ML-files that do not
-belong to a theory (see explanation of $theoryDef$ in \ref{DefiningTheories}).
-These files are read manually between {\tt use_thy} calls and define objects
-used in different theories.  As {\tt update} only knows about the
-theories there still exist objects with references to the old theory version
-after the new one has been read.  This (most probably) will produce the fatal
-error
+There is a problem with \ttindex{update}: objects created in \ML-files that do
+not belong to a theory (see explanation of $theoryDef$ in
+\ref{DefiningTheories}).  These files are read manually between {\tt use_thy}
+calls and define objects used in different theories.  As {\tt update} only
+knows about the theories there still exist objects with references to the old
+theory version after the new one has been read.  This (most probably) will
+produce the fatal error
 \begin{center} \tt
 Attempt to merge different versions of theory: $T$
 \end{center}
@@ -227,15 +229,18 @@
 
 
 \subsection{Removing a theory}
+\index{removing theories}
 
-If a previously read file is removed the {\tt update} function will keep
+If a previously read file is removed the \ttindex{update} function will keep
 on complaining about a missing file.  The theory is not automatically removed
 from the internal list to preserve the links to other theories in case one
 forgot to adjust the {\tt loadpath} after moving a file.  To manually remove a
-theory use {\tt unlink_thy}.
+theory use \ttindexbold{unlink_thy}.
 
 
 \subsection{Using Poly/\ML}
+\index{Poly/\ML}
+\index{reference variables}
 
 As the functions for reading theories depend on reference variables one has to
 take into consideration the way Poly/\ML{} handles them.  They are only saved
@@ -245,14 +250,12 @@
 structure has to be declared by
 \begin{ttbox}
 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+Readthy.loaded_thys := !loaded_thys;
 open Readthy;
 \end{ttbox}
-in every newly created database.  This is not necessary if the database is
-created by copying an existent one.
-
-%The above declarations are contained in the $Pure$ database, so one could
-%simply use e.g. {\tt use_thy} if saving of the reference variables is not
-%needed.  Standard ML of New Jersey does not have this behaviour.
+in every newly created database.  By copying the contents of the old reference
+variable loaded_thys the list of already loaded theories is preserved. Of
+course this is not necessary if no theories have been read yet.
 
 
 \section{Basic operations on theories}