Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-23 19:24:37 -0700 (Thu, 23 Oct 2003)
Revision: 5035
Log message:

      - This fixes all-theories.pdf build (bug 57)
      
      - In bytecode mode, omake should use mp.top, not mp.opt
      
      - Made ocamldep -prl mode a bit smarter:
      a) When a PRL .mli file contains "mptop", then .cmi dependes on Shell_sig and Mptop
      modules
      b) When a PRL file contains "interactive", "interactive_rw" or "derived", then it
      depeneds on the Shell module
      c) All PRL .cmx and .cmo files depend on Shell_sig and Mptop signatures (strictly speaking,
      this is only true when the corresponding .mli contains an "mptop" directive), but this is an
      approximation
      
      - Printexn.catch is a bad idea now (the runtime now is as good at printing uncaught
      exceptions and Printexn.catch blocks exception backtracing), got rid of all of them.
      
      - Print a better error message when trying to cd into a theory that does not exist.
      
      - The all-theories theory list was missing the base_theory file, and the fol_theory one
      should not be there.
      
      - Minor changes in module (AKA theory, AKA package) management in shell.
      
      - Made "omake clean" in editor/ml a bit cleaner
      

Changes  Path
+1 -1 metaprl/OMakefile
+1 -3 metaprl/debug/debug.ml
+2 -2 metaprl/editor/ml/OMakefile
+20 -20 metaprl/editor/ml/shell_p4.ml
+0 -1 metaprl/editor/ml/tests/czf.ml
+1 -2 metaprl/filter/filter/filter_bin.ml
+1 -2 metaprl/filter/filter/filter_convert.ml
+1 -1 metaprl/filter/filter/prlcomp.ml
+14 -0 metaprl/refiner/reflib/theory.ml
+1 -0 metaprl/refiner/reflib/theory.mli
+3 -30 metaprl/support/shell/package_info.ml
+1 -0 metaprl/support/shell/package_sig.mlz
+15 -15 metaprl/support/shell/shell.ml
+0 -1 metaprl/support/shell/shell.mli
+0 -1 metaprl/support/shell/shell_sig.mlz
+1 -1 metaprl/tactics/ensemble/appl_ensemble.ml
+1 -1 metaprl/tactics/ensemble/appl_outboard_server.ml
+1 -0 metaprl/theories/base/OMakefile
+0 -1 metaprl/theories/fol/OMakefile
+3 -3 metaprl/util/check-status.sh
+31 -13 metaprl/util/ocamldep.mll