src/Pure/Thy/read.ML
1994-05-26 clasohm 1994-05-26 changed syntax of use_string
1994-05-19 clasohm 1994-05-19 use_thy now uses use_string instead of creating a temporary file
1994-04-24 clasohm 1994-04-24 fixed a small bug
1994-04-24 clasohm 1994-04-24 changed convention for theory file names: they now have to consist of the exact theory name + extension
1994-02-16 clasohm 1994-02-16 moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
1994-02-02 clasohm 1994-02-02 made error message "file not found" more informative
1994-01-10 clasohm 1994-01-10 added a check for existence of a temporary file before removing it
1994-01-05 nipkow 1994-01-05 shortened msg
1993-12-30 clasohm 1993-12-30 added "Reading thy-File" message
1993-12-22 clasohm 1993-12-22 fixed a bug in update/next_level which occured when a child wasn't loaded
1993-11-25 clasohm 1993-11-25 fixed a bug in get_filenames, changed output of use_thy
1993-11-16 clasohm 1993-11-16 added loaded_thys to signature and removed list_/set_loaded
1993-11-16 clasohm 1993-11-16 moved call of store_theory to end of use t.thy; use t.ML; use_thy now needs the exact theory name (capital/lower letters); improved handling of incompletly read theories; added function unlink_thy, removed function relations; added reference variable delete_tmpfile; removed some bugs
1993-10-26 clasohm 1993-10-26 corrected some spelling mistakes; removed a bug that made it impossible to read theories that don't have a ML file; extended syntax for bases in syntax.ML: a string can be used to specify a theory that is to be read but is not merged into the base (useful for pseudo theories used to document the dependencies of ML files)
1993-10-22 clasohm 1993-10-22 removed a bug that occured when a path was specified for use_thy's parameter and the theory was created in a .ML file
1993-10-22 clasohm 1993-10-22 changes in Readthy: - reads needed base theories automatically - keeps a time stamp for all read files - update function - checks for cycles - path list that is searched for files - reads theories that are created in .ML files - etc.
1993-09-16 clasohm 1993-09-16 Initial revision