# HG changeset patch
# User clasohm
# Date 803901546 -7200
# Node ID da78c293e8dccb236e34c0da0304144852b84e7d
# Parent  b373cb33352fcbf8b9b1f27fc41fe324b06929cd
added a few comments on ThyInfo

diff -r b373cb33352f -r da78c293e8dc src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Jun 23 09:15:09 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Jun 23 11:59:06 1995 +0200
@@ -4,21 +4,25 @@
                 Tobias Nipkow and L C Paulson
     Copyright   1994 TU Muenchen
 
-(* FIXME !? *)
-Reading and writing the theory definition files.
-
-(* FIXME !? *)
-For theory XXX, the  input file is called XXX.thy
-                the output file is called .XXX.thy.ML
-                and it then tries to read XXX.ML
+Functions for reading theory files, and storing and retrieving theories
+and theorems.
 *)
 
+(*Type for theory storage*)
 datatype thy_info = ThyInfo of {path: string,
                                 children: string list,
                                 thy_time: string option,
                                 ml_time: string option,
                                 theory: theory option,
                                 thms: thm Symtab.table};
+      (*meaning of special values:
+        thy_time, ml_time = None     theory file has not been read yet
+                          = Some ""  theory was read but has either been marked
+                                     as outdated or there is no such file for
+                                     this theory (see e.g. 'virtual' theories
+                                     like Pure or theories without a ML file)
+        theory = None  theory has not been read yet
+       *)
 
 signature READTHY =
 sig