added index commands, removed last paragraph of "Using Poly/ML"
authorclasohm
Thu Nov 25 10:29:40 1993 +0100 (1993-11-25)
changeset 141a133921366cb
parent 140 3a8c68d1d466
child 142 6dfae8cddec7
added index commands, removed last paragraph of "Using Poly/ML"
doc-src/Ref/introduction.tex
doc-src/Ref/ref.toc
doc-src/Ref/theories.tex
     1.1 --- a/doc-src/Ref/introduction.tex	Tue Nov 23 10:47:33 1993 +0100
     1.2 +++ b/doc-src/Ref/introduction.tex	Thu Nov 25 10:29:40 1993 +0100
     1.3 @@ -94,9 +94,7 @@
     1.4  time_use        : string -> unit
     1.5  time_use_thy    : string -> unit
     1.6  update          : unit -> unit
     1.7 -unlink_thy      : string -> unit
     1.8  loadpath        : string list ref
     1.9 -delete_tmpfiles : bool ref
    1.10  \end{ttbox}
    1.11  \begin{description}
    1.12  \item[\ttindexbold{cd} \tt"{\it dir}";]  changes to {\it dir\/} the default
    1.13 @@ -123,18 +121,9 @@
    1.14  reads all theories that have changed since the last time they have been read.
    1.15  See Chapter~\ref{theories} for details.
    1.16  
    1.17 -\item[\ttindexbold{unlink_thy} \tt"$tname$";]  
    1.18 -removes theory {\it tname} from internal list of theory dependencies and has to
    1.19 -be used after removing a theory's files. Else {\tt update} would keep on
    1.20 -searching for them. See Chapter~\ref{theories} for details.
    1.21 -
    1.22  \item[\ttindexbold{loadpath}] contains a list of paths that is used by 
    1.23  {\tt use_thy} and {\tt update} to find {\it tname}{\tt.ML} and {\it tname}
    1.24  {\tt.thy}. See Chapter~\ref{theories} for details.
    1.25 -
    1.26 -\item[\ttindexbold{delete_tmpfiles}] is used by use_thy and controls the
    1.27 -removal of temporary files created during the reading of {\it tname}{\tt.thy}.
    1.28 -See Chapter~\ref{theories} for details.
    1.29  \end{description}
    1.30  
    1.31  
     2.1 --- a/doc-src/Ref/ref.toc	Tue Nov 23 10:47:33 1993 +0100
     2.2 +++ b/doc-src/Ref/ref.toc	Thu Nov 25 10:29:40 1993 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  \contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3}
     2.5  \contentsline {subsection}{Printing limits}{3}
     2.6  \contentsline {subsection}{Printing of meta-level hypotheses}{3}
     2.7 -\contentsline {subsection}{Printing of types and sorts}{4}
     2.8 +\contentsline {subsection}{Printing of types and sorts}{3}
     2.9  \contentsline {subsection}{$\eta $-contraction before printing}{4}
    2.10  \contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
    2.11  \contentsline {section}{\numberline {1.6}Shell scripts}{5}
     3.1 --- a/doc-src/Ref/theories.tex	Tue Nov 23 10:47:33 1993 +0100
     3.2 +++ b/doc-src/Ref/theories.tex	Thu Nov 25 10:29:40 1993 +0100
     3.3 @@ -157,12 +157,13 @@
     3.4  
     3.5  
     3.6  \subsection{Filenames and paths}
     3.7 +\indexbold{filenames}
     3.8  
     3.9  The files the theory definition resides in must have the lower case name of
    3.10 -the theory with ".thy" or ".ML" appended.  On the other hand {\tt use_thy}'s
    3.11 +the theory with ".thy" or ".ML" appended.  On the other hand \ttindex{use_thy}'s
    3.12  parameter has to be the exact theory name.  Optionally the name can be
    3.13  preceeded by a path to specify the directory where the files can be found.  If
    3.14 -no path is provided the reference variable {\tt loadpath} is used which
    3.15 +no path is provided the reference variable \ttindexbold{loadpath} is used which
    3.16  contains a list of paths that are searched in the given order.  After the
    3.17  ".thy"-file for a theory has been found, the same path is used to locate the
    3.18  (optional) ".ML"-file.  (You might note that it is also possible to only
    3.19 @@ -173,33 +174,34 @@
    3.20  
    3.21  
    3.22  \subsection{Reloading a theory}
    3.23 +\index{reloading a theory}
    3.24  
    3.25 -{\tt use_thy} keeps track of all loaded theories and stores information about
    3.26 -their files.  If it finds that the theory to be loaded was already read
    3.27 +\ttindex{use_thy} keeps track of all loaded theories and stores information
    3.28 +about their files.  If it finds that the theory to be loaded was already read
    3.29  before, the following happens: First the theory's files are searched at the
    3.30 -place they were located the last time they were read. If they are found,
    3.31 -their time of last modification is compared to the internal data and {\tt
    3.32 -  use_thy} stops if they are equal. In case the files have been moved, {\tt
    3.33 -  use_thy} searches them the same way a new theory would be searched for.
    3.34 -After all these tests have been passed, the theory is reloaded and all
    3.35 -theories that depend on it (i.e. that have its name in their $theoryDef$) are
    3.36 -marked as out-of-date.
    3.37 +place they were located the last time they were read. If they are found, their
    3.38 +time of last modification is compared to the internal data and {\tt use_thy}
    3.39 +stops if they are equal. In case the files have been moved, {\tt use_thy}
    3.40 +searches them the same way a new theory would be searched for.  After all these
    3.41 +tests have been passed, the theory is reloaded and all theories that depend on
    3.42 +it (i.e. that have its name in their $theoryDef$) are marked as out-of-date.
    3.43  
    3.44  As changing a theory often makes it necessary to reload all theories that
    3.45 -(indirectly) depend on it, {\tt update} should be used instead of {\tt
    3.46 +(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt
    3.47  use_thy} to read a modified theory.  This function reloads all changed
    3.48  theories and their descendants in the correct order.
    3.49  
    3.50  
    3.51  \subsection{Pseudo theories}
    3.52 +\indexbold{pseudo theories}
    3.53  
    3.54 -There is a problem with {\tt update}: objects created in \ML-files that do not
    3.55 -belong to a theory (see explanation of $theoryDef$ in \ref{DefiningTheories}).
    3.56 -These files are read manually between {\tt use_thy} calls and define objects
    3.57 -used in different theories.  As {\tt update} only knows about the
    3.58 -theories there still exist objects with references to the old theory version
    3.59 -after the new one has been read.  This (most probably) will produce the fatal
    3.60 -error
    3.61 +There is a problem with \ttindex{update}: objects created in \ML-files that do
    3.62 +not belong to a theory (see explanation of $theoryDef$ in
    3.63 +\ref{DefiningTheories}).  These files are read manually between {\tt use_thy}
    3.64 +calls and define objects used in different theories.  As {\tt update} only
    3.65 +knows about the theories there still exist objects with references to the old
    3.66 +theory version after the new one has been read.  This (most probably) will
    3.67 +produce the fatal error
    3.68  \begin{center} \tt
    3.69  Attempt to merge different versions of theory: $T$
    3.70  \end{center}
    3.71 @@ -227,15 +229,18 @@
    3.72  
    3.73  
    3.74  \subsection{Removing a theory}
    3.75 +\index{removing theories}
    3.76  
    3.77 -If a previously read file is removed the {\tt update} function will keep
    3.78 +If a previously read file is removed the \ttindex{update} function will keep
    3.79  on complaining about a missing file.  The theory is not automatically removed
    3.80  from the internal list to preserve the links to other theories in case one
    3.81  forgot to adjust the {\tt loadpath} after moving a file.  To manually remove a
    3.82 -theory use {\tt unlink_thy}.
    3.83 +theory use \ttindexbold{unlink_thy}.
    3.84  
    3.85  
    3.86  \subsection{Using Poly/\ML}
    3.87 +\index{Poly/\ML}
    3.88 +\index{reference variables}
    3.89  
    3.90  As the functions for reading theories depend on reference variables one has to
    3.91  take into consideration the way Poly/\ML{} handles them.  They are only saved
    3.92 @@ -245,14 +250,12 @@
    3.93  structure has to be declared by
    3.94  \begin{ttbox}
    3.95  structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
    3.96 +Readthy.loaded_thys := !loaded_thys;
    3.97  open Readthy;
    3.98  \end{ttbox}
    3.99 -in every newly created database.  This is not necessary if the database is
   3.100 -created by copying an existent one.
   3.101 -
   3.102 -%The above declarations are contained in the $Pure$ database, so one could
   3.103 -%simply use e.g. {\tt use_thy} if saving of the reference variables is not
   3.104 -%needed.  Standard ML of New Jersey does not have this behaviour.
   3.105 +in every newly created database.  By copying the contents of the old reference
   3.106 +variable loaded_thys the list of already loaded theories is preserved. Of
   3.107 +course this is not necessary if no theories have been read yet.
   3.108  
   3.109  
   3.110  \section{Basic operations on theories}