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%.