Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-07 00:02:30 -0700 (Fri, 07 Jul 2000)
Revision: 3021
Log message:

      - Fixed the unquoting problem that caused some .prla files to be misread.
      This required fixing the String_util.parse_args to fully match String_util.quote.
      Unfortunatelly, parse_args is used in several places - hopefully I didn't break
      any of those.
      
      - Added several TODO items.
      
      - Made sure we set LC_ALL=C to avoid the problem with different people creating different
      .prla files based on their locale settings.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-10 22:04:33 -0700 (Mon, 10 Jul 2000)
Revision: 3023
Log message:

      Additional debugging.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-11 23:30:51 -0700 (Tue, 11 Jul 2000)
Revision: 3024
Log message:

      - Do not forget to reset the proof item address before leaving the item.
      - Debugging exhancement and small bugfixes in proof_boot.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-16 15:54:54 -0700 (Sun, 16 Jul 2000)
Revision: 3025
Log message:

      More TODO items.
      Some debugging code in Boot - trying to figure the withT leaking problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-17 16:16:52 -0700 (Mon, 17 Jul 2000)
Revision: 3026
Log message:

      TODO - updated after first round of discussion with Jason.
      
      filter - fixed the bug with with*T leaking goal annotations.
      I still need to clean up the proofs where the annotations were already leaked
      
      refiner - ascii_io now allows one to read any line from an ASCII file (not only
      the last line which represent the whole file). Useful for debugging.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-19 22:39:03 -0700 (Wed, 19 Jul 2000)
Revision: 3027
Log message:

      Backported some of Jason's changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-20 01:01:41 -0700 (Thu, 20 Jul 2000)
Revision: 3028
Log message:

      Squah away attributes at unjustified nodes (still need to figure out why
      they reappear sometimes).
      
      Removed some "empty" .prla files (not all of them).
      
      Updated TODO after talking more to Jason (notice that TODO is now private and
      only accessable by people with valid MetaPRL CVS accounts).
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-07-20 17:58:24 -0700 (Thu, 20 Jul 2000)
Revision: 3029
Log message:

      Added readline input handling.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-25 10:22:43 -0700 (Tue, 25 Jul 2000)
Revision: 3030
Log message:

      TODO - ocamldebug and ocamlprof support.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-07-25 10:24:20 -0700 (Tue, 25 Jul 2000)
Revision: 3031
Log message:

      Fixed the problem with loading multiple theories that share
      a common theory (BUGS 2.3).  Still have a problem with displaying
      terms correctly in the toplevel.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-07-25 16:10:51 -0700 (Tue, 25 Jul 2000)
Revision: 3032
Log message:

      Fixed the problem with loading and editing several theories that have common
      parents.
      
      Fixed a problem with bytecode make forgetting to do things in filter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-25 17:00:24 -0700 (Tue, 25 Jul 2000)
Revision: 3033
Log message:

      Better display forms for raw IO terms.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-25 19:10:31 -0700 (Tue, 25 Jul 2000)
Revision: 3034
Log message:

      debug_base display form base should be in Dform, not in Proof_boot.Proof
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-26 13:50:16 -0700 (Wed, 26 Jul 2000)
Revision: 3035
Log message:

      Moved the debugging (format_*) code around. Added more of it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-27 12:55:54 -0700 (Thu, 27 Jul 2000)
Revision: 3036
Log message:

      - Fixed the problem with leaking attributes.
      
      - Fixed the problem with top-level functions (such as clean_all)
      removing the "Primivive" flag and replacing it with "Interactive".
      
      - Fixed some display forms.
      
      - Removed "empty" .prla files in ITT and "refreshed" the rest of them.
      
      - More in BUGS and TODO.
      
      - Other small changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-27 15:32:59 -0700 (Thu, 27 Jul 2000)
Revision: 3037
Log message:

      Threat other "serious" exceptions from Pervasives in the same way as Invalid_argument.