Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-16 18:31:36 -0700 (Thu, 16 Apr 1998)
Revision: 2137
Log message:

      Editor is almost constructed.
      

Changes	Path
+2 -5	metaprl/editor/ml/Makefile
Deleted	metaprl/editor/ml/display_package.ml
Deleted	metaprl/editor/ml/display_package.mli
Deleted	metaprl/editor/ml/display_package_graph.ml
Deleted	metaprl/editor/ml/display_package_graph.mli
Deleted	metaprl/editor/ml/display_theory_item.ml
Deleted	metaprl/editor/ml/display_theory_item.mli
Deleted	metaprl/editor/ml/package_graph.ml
Deleted	metaprl/editor/ml/package_graph.mli
+117 -41	metaprl/editor/ml/package_info.ml
+6 -1	metaprl/editor/ml/package_type.mlz
+28 -25	metaprl/editor/ml/proof.ml
+5 -2	metaprl/editor/ml/proof.mli
+12 -9	metaprl/editor/ml/proof_step.ml
+4 -1	metaprl/editor/ml/proof_step.mli
+90 -161	metaprl/editor/ml/shell.ml
+35 -46	metaprl/editor/ml/shell.mli
Properties	metaprl/filter
+3 -2	metaprl/filter/Makefile
+13 -4	metaprl/filter/filter_cache.ml
+5 -1	metaprl/filter/filter_cache.mli
+86 -80	metaprl/filter/filter_cache_fun.ml
Added	metaprl/filter/filter_proof.ml
Properties	metaprl/filter/filter_proof.ml
Added	metaprl/filter/filter_proof.mli
Properties	metaprl/filter/filter_proof.mli
Added	metaprl/filter/filter_proof_type.mlz
Properties	metaprl/filter/filter_proof_type.mlz
+7 -2	metaprl/filter/filter_summary.ml
+4 -0	metaprl/filter/filter_summary_type.mlz
Deleted	metaprl/filter/proof_type.mlz
+4 -0	metaprl/mllib/dag.mlz
+4 -1	metaprl/mllib/imp_dag.ml
+16 -9	metaprl/refiner/term.ml
Properties	metaprl/theories/base
+2 -0	metaprl/theories/base/Makefile
+5 -0	metaprl/theories/base/base_theory.mlz
+9 -0	metaprl/theories/base/nuprl_font.ml
+6 -0	metaprl/theories/base/nuprl_font.mli
Added	metaprl/theories/base/perv.ml
Properties	metaprl/theories/base/perv.ml
Added	metaprl/theories/base/perv.mli
Properties	metaprl/theories/base/perv.mli
Added	metaprl/theories/base/summary.ml
Properties	metaprl/theories/base/summary.ml
Added	metaprl/theories/base/summary.mli
Properties	metaprl/theories/base/summary.mli
+4 -1	metaprl/theories/tactic/tactic_type.mlz
+4 -1	metaprl/theories/tactic/tacticals.ml