Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-17 17:17:59 -0700 (Thu, 17 Jun 2004)
Revision: 5920
Log message:

      1) This makes a major change in how the relative addresses are handled
      in proof editing. Now the Proof.proof type is just a Proof.extract and
      proofs no longer keep the subaddress (relative address) internaly.
      Instead, the relative address is kept by the shell and is passed functionally
      to all the edit_* functions that need it.
      
      The only module that keeps its own copy of the relative address is Shell_fs
      (should be easy to fix, but I wanted to leave this up to Jason).
      
      Undo/Redo functions now explicitly return the new (or old, depending on
      how you look at it) relative address.
      
      2) Minor proof updates in itt_list2
      

Changes  Path
+1 -1 metaprl/support/shell/inputs/login.html
+2 -2 metaprl/support/shell/package_info.ml
+105 -154 metaprl/support/shell/proof_edit.ml
+7 -12 metaprl/support/shell/proof_edit.mli
+20 -23 metaprl/support/shell/shell.ml
+1 -2 metaprl/support/shell/shell.mli
+128 -163 metaprl/support/shell/shell_core.ml
+1 -1 metaprl/support/shell/shell_core.mli
+23 -36 metaprl/support/shell/shell_current.ml
+18 -35 metaprl/support/shell/shell_fs.ml
+6 -4 metaprl/support/shell/shell_internal_sig.mlz
+5 -9 metaprl/support/shell/shell_package.ml
+13 -16 metaprl/support/shell/shell_root.ml
+25 -33 metaprl/support/shell/shell_rule.ml
+9 -20 metaprl/support/shell/shell_sig.mlz
+1 -1 metaprl/support/shell/shell_syscall.ml
+2 -2 metaprl/tactics/proof/exn_boot.ml
+259 -443 metaprl/tactics/proof/proof_boot.ml
+17 -32 metaprl/tactics/proof/tactic_boot_sig.ml
+568 -601 metaprl/theories/itt/itt_list2.prla