Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-12-23 00:10:57 -0800 (Mon, 23 Dec 2002)
Revision: 3973
Log message:

      - We used to generase resource "bookmarks" (checkpoints) for all
      the rules/rewrites. Now only interactive/derived/incomplete rules/rewrites
      would have checkpoints while primitive/ml ones would not
      
      - Fixed a bug with resource management (in case where a theory include
      is followed by a resource improvement as opposed to being followed by a bookmark,
      the included data was not inherited)
      
      - Creating a rule/rewrite "edit" object should not require finding a sentinel
      and bookmark (those are only needed only when we want to edit the actual proof).
      
      P.S. This commit have sped up the "status_all" by about 12%.
      

Changes  Path
+10 -16 metaprl/editor/ml/shell_rewrite.ml
+10 -16 metaprl/editor/ml/shell_rule.ml
+41 -47 metaprl/filter/base/filter_prog.ml
+2 -2 metaprl/refiner/reflib/mp_resource.ml
+7 -1 metaprl/util/check-status.sh