Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-08 17:58:52 -0800 (Tue, 08 Feb 2005)
Revision: 6637
Log message:

      Improve the space used by MetaPRL.
      
      The "abandon ()" command abandons the current theory.
      CAUTION: use this only if you want to lose your unsaved
      work.  You will not be prompted.
      
      The "abandon_all ()" command tries to get MetaPRL back to
      startup state.  It abandons all theories, all caches, all
      file information, and the proof cache.
      
      Package_info is now saved in a Weak array.  This means that
      the package info for unmodified theories can be garbage collected.
      
      To check status without saving, use
         status_and_abandon_all ().
      This will delete all your unsaved work.
      
      We still have some memory leaks.  After a status_and_abandon_all,
      we have roughly 160MB live data.  MetaPRL starts with 20MB.
      I've covered these:
         1. The file base: file_base.ml
         2. The proof cache: proof_boot.ml
         3. The filter: filter_cache_fun.ml
         4. The package_info: package_info.ml
         5. Some of the resource data: mp_resource.ml
      
      It looks like some other place is caching data...
      

Changes  Path
+7 -0 metaprl/filter/base/filter_cache_fun.ml
+2 -1 metaprl/filter/base/filter_summary_io.ml
+2 -0 metaprl/filter/base/filter_summary_type.ml
+3 -1 metaprl/mllib/file_base.ml
+2 -1 metaprl/mllib/file_base_type.ml
+143 -71 metaprl/support/shell/package_info.ml
+10 -8 metaprl/support/shell/package_info.mli
+0 -0 metaprl/support/shell/proof_edit.ml
+28 -20 metaprl/support/shell/shell.ml
+63 -20 metaprl/support/shell/shell_command.ml
+10 -0 metaprl/support/shell/shell_command.mli
+57 -31 metaprl/support/shell/shell_core.ml
+19 -10 metaprl/support/shell/shell_core.mli
+9 -2 metaprl/support/shell/shell_sig.mlz
+6 -3 metaprl/tactics/proof/proof_boot.ml
+4 -0 metaprl/tactics/proof/tactic_boot_sig.ml
+1 -1 metaprl/theories/itt/itt_synt_bterm.mli
+1 -1 metaprl/util/status-all.sh