Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-18 16:04:33 -0700 (Fri, 18 Jun 2004)
Revision: 5943
Log message:

      - Do not die on entering a primitive item (is_edit_enabled needed to return
      false right away, without trying to go through Proof_edit in that case).
      
      - Proof_info needs to write .cmoz using a "non-interactive" magic (to allow
      the compiler to overwrite them). Note that the flags are maintained
      imperatively, so the whole setup ends up being a big hack. :-(
      

Changes	Path
+3 -1	metaprl/mllib/file_type_base.ml
+5 -0	metaprl/support/shell/package_info.ml
+6 -1	metaprl/support/shell/shell_rule.ml