Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-04-18 18:46:53 -0700 (Sun, 18 Apr 2004)
Revision: 5668
Log message:

      This is an annoying commit.  It looks massive, but many of the changes
      are just to "open" statements.  Here is the issue that is addressed.
         1. Format is a superset of Printf, and it is much better.
         2. MetaPRL's Rformat is a superset of Format, and it is much better.
      
      This commit moves Rformat into libmojave, as Lm_rformat.  With this
      commit, all output normally goes through Lm_rformat.  Feel free to
      continue to use Format/Printf in special cases, but normal user output
      should go through Lm_format/Lm_printf.  You will probably need to use
      Lm_pervasives as well.
      
      Lm_pervasives defines an (output_rbuffer : out_channel -> Lm_buffer.t -> unit)
      that should be used instead of the print_text_channel function.
      
      There is a new FORMAT option in mk/config.  Define FORMAT=Format to
      enable old behavior if you have trouble.
      
      There are two reasons behind this:
         1. We had a mix of files that use Printf and those that use Format
            for output.  This was a mess.  For instance format-style print
            directives (like "@[<hv 3>Content of text box@]@.") can't be
            used in raw Printf.  This meant that output functions had
            to be duplicated, one version for Printf, and one for Format.
            This commit solves the problem.
         2. Another reason, and the real reason behind this, is to allow
            output to be diverted based on the display device.
      

Changes  Path
Properties metaprl
+28 -3 metaprl/OMakefile
+1 -1 metaprl/debug/debug.ml
+1 -1 metaprl/debug/debug_symbols.ml
+2 -2 metaprl/editor/ml/make_mp_version.ml
+1 -2 metaprl/editor/ml/mp.ml
+1 -1 metaprl/editor/ml/mp_top.ml
+2 -2 metaprl/editor/ml/nuprl_eval.ml
+1 -0 metaprl/editor/ml/nuprl_run.ml
+15 -19 metaprl/editor/ml/shell_mp.ml
+8 -9 metaprl/editor/ml/shell_p4.ml
+5 -6 metaprl/editor/ml/tests/czf.ml
+1 -1 metaprl/editor/ml/tests/pigeon.ml
+1 -1 metaprl/editor/ml/tests/prop-pigeon.ml
+3 -4 metaprl/editor/ml/tests/seq_addrs_test.ml
+1 -2 metaprl/editor/ml/tutorial.ml
+1 -2 metaprl/editor/ml/tutorial_itt.ml
+1 -1 metaprl/editor/ml/x.ml
+5 -4 metaprl/filter/base/filter_buffer.ml
+6 -5 metaprl/filter/base/filter_cache.ml
+2 -2 metaprl/filter/base/filter_cache_fun.ml
+1 -0 metaprl/filter/base/filter_comment.ml
+123 -113 metaprl/filter/base/filter_exn.ml
+1 -1 metaprl/filter/base/filter_exn.mli
+1 -0 metaprl/filter/base/filter_hash.ml
+3 -3 metaprl/filter/base/filter_ocaml.ml
+5 -5 metaprl/filter/base/filter_spell.ml
+3 -2 metaprl/filter/base/filter_summary.ml
+2 -1 metaprl/filter/base/filter_summary_io.ml
+1 -0 metaprl/filter/base/filter_summary_util.ml
+1 -0 metaprl/filter/base/filter_util.ml
+1 -1 metaprl/filter/base/free_vars.ml
+1 -0 metaprl/filter/base/mLast_util.ml
+1 -1 metaprl/filter/filter/filter_bin.ml
+1 -0 metaprl/filter/filter/filter_convert.ml
+3 -3 metaprl/filter/filter/filter_main.ml
+7 -7 metaprl/filter/filter/filter_parse.ml
+2 -2 metaprl/filter/filter/filter_prog.ml
+3 -2 metaprl/filter/filter/prlcomp.ml
+4 -3 metaprl/filter/filter/term_grammar.ml
+1 -2 metaprl/filter/phobos/phobos_constants.ml
+55 -54 metaprl/filter/phobos/phobos_debug.ml
+15 -13 metaprl/filter/phobos/phobos_exn.ml
+2 -1 metaprl/filter/phobos/phobos_exn.mli
+4 -4 metaprl/filter/phobos/phobos_grammar.ml
+41 -41 metaprl/filter/phobos/phobos_main.ml
+4 -4 metaprl/filter/phobos/phobos_parse_state.ml
+2 -2 metaprl/filter/phobos/phobos_parse_state.mli
+4 -4 metaprl/filter/phobos/phobos_parser.mly
+89 -89 metaprl/filter/phobos/phobos_print.ml
+20 -20 metaprl/filter/phobos/phobos_report.ml
+1 -0 metaprl/filter/phobos/phobos_state.ml
+3 -3 metaprl/filter/phobos/phobos_tokenizer.ml
+16 -17 metaprl/filter/phobos/phobos_util.ml
+5 -4 metaprl/library/ascii_scan.ml
+1 -11 metaprl/library/basic.ml
+5 -7 metaprl/library/bigInt.ml
+2 -1 metaprl/library/db.ml
+14 -18 metaprl/library/definition.ml
+8 -8 metaprl/library/library.ml
+5 -5 metaprl/library/library_type_base.ml
+1 -0 metaprl/library/link.ml
+3 -1 metaprl/library/lint32.ml
+1 -0 metaprl/library/mathBus.ml
+2 -1 metaprl/library/mbterm.ml
+1 -0 metaprl/library/nuprl5.ml
+5 -5 metaprl/library/object_id.ml
+5 -4 metaprl/library/oidtable.ml
+1 -0 metaprl/library/orb.ml
+1 -0 metaprl/library/registry.ml
+6 -5 metaprl/library/socketIo.ml
+5 -5 metaprl/library/tentfunctor.ml
+1 -1 metaprl/library/test.ml
+11 -10 metaprl/library/utils.ml
+1 -0 metaprl/mk/defaults
+6 -0 metaprl/mk/make_config.sh
+1 -0 metaprl/mllib/bitset.ml
+2 -2 metaprl/mllib/debug_string_sets.ml
+1 -1 metaprl/mllib/debug_tables.ml
+1 -1 metaprl/mllib/env_arg.ml
+2 -2 metaprl/mllib/file_base.ml
+1 -1 metaprl/mllib/file_type_base.ml
+16 -3 metaprl/mllib/http_server.ml
+5 -2 metaprl/mllib/http_simple.ml
+1 -1 metaprl/mllib/memo.ml
+1 -1 metaprl/mllib/mp_term.ml
+1 -0 metaprl/mllib/precedence.ml
+2 -2 metaprl/mllib/remote_queue_null.ml
+1 -1 metaprl/mllib/weak_memo.ml
+1 -0 metaprl/refiner/refbase/opname.ml
+3 -2 metaprl/refiner/refiner/refine.ml
+0 -1 metaprl/refiner/reflib/Files
+4 -3 metaprl/refiner/reflib/arith.ml
+2 -2 metaprl/refiner/reflib/ascii_io.ml
+4 -5 metaprl/refiner/reflib/ascii_io_sig.ml
+11 -9 metaprl/refiner/reflib/dform.ml
+2 -1 metaprl/refiner/reflib/dform.mli
+303 -301 metaprl/refiner/reflib/jall.ml
+3 -3 metaprl/refiner/reflib/jtunify.ml
+1 -0 metaprl/refiner/reflib/match_seq.ml
+2 -2 metaprl/refiner/reflib/mp_resource.ml
+8 -6 metaprl/refiner/reflib/refine_exn.ml
+1 -1 metaprl/refiner/reflib/refine_exn.mli
Deleted metaprl/refiner/reflib/rformat.ml
Deleted metaprl/refiner/reflib/rformat.mli
+40 -29 metaprl/refiner/reflib/simple_print.ml
+0 -0 metaprl/refiner/reflib/simple_print.mli
+2 -1 metaprl/refiner/reflib/simple_print_sig.ml
+259 -258 metaprl/refiner/reflib/supinf.ml
+1 -0 metaprl/refiner/reflib/term_compare.ml
+1 -0 metaprl/refiner/reflib/term_dtable.ml
+2 -2 metaprl/refiner/reflib/term_match_table.ml
+2 -1 metaprl/refiner/reflib/term_stable.ml
+1 -0 metaprl/refiner/reflib/term_stable.mli
+2 -1 metaprl/refiner/reflib/theory.ml
+0 -0 metaprl/refiner/refsig/refiner_sig.ml
+1 -0 metaprl/refiner/refsig/term_base_sig.ml
+2 -1 metaprl/refiner/refsig/term_shape_sig.ml
+1 -0 metaprl/refiner/refsig/thread_refiner_sig.ml
+3 -2 metaprl/refiner/rewrite/rewrite.ml
+3 -2 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+2 -1 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+2 -1 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+2 -1 metaprl/refiner/rewrite/rewrite_debug.ml
+1 -0 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+3 -2 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -0 metaprl/refiner/rewrite/rewrite_util.ml
+1 -2 metaprl/refiner/term_ds/rob_ds.ml
+3 -2 metaprl/refiner/term_ds/term_base_ds.ml
+2 -1 metaprl/refiner/term_ds/term_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+2 -1 metaprl/refiner/term_ds/term_man_ds.ml
+3 -2 metaprl/refiner/term_ds/term_subst_ds.ml
+2 -1 metaprl/refiner/term_gen/term_man_gen.ml
+6 -5 metaprl/refiner/term_gen/term_shape_gen.ml
+2 -0 metaprl/refiner/term_std/term_base_std.ml
+2 -1 metaprl/refiner/term_std/term_std.ml
+1 -0 metaprl/refiner/term_std/term_std_sig.ml
+3 -2 metaprl/refiner/term_std/term_subst_std.ml
+3 -2 metaprl/support/display/base_dform.ml
+2 -1 metaprl/support/display/nuprl_font.ml
+1 -0 metaprl/support/display/ocaml_base_df.ml
+1 -0 metaprl/support/display/ocaml_expr_df.ml
+1 -0 metaprl/support/display/ocaml_me_df.ml
+1 -0 metaprl/support/display/ocaml_mt_df.ml
+1 -0 metaprl/support/display/ocaml_patt_df.ml
+1 -0 metaprl/support/display/ocaml_sig_df.ml
+1 -0 metaprl/support/display/ocaml_str_df.ml
+1 -0 metaprl/support/display/ocaml_type_df.ml
+1 -0 metaprl/support/display/perv.ml
+1 -0 metaprl/support/display/summary.ml
+2 -2 metaprl/support/shell/browser_display_term.ml
+2 -2 metaprl/support/shell/browser_display_term.mli
+4 -5 metaprl/support/shell/java_display_term.ml
+10 -8 metaprl/support/shell/java_mux_channel.ml
+2 -2 metaprl/support/shell/package_info.ml
+337 -301 metaprl/support/shell/proof_edit.ml
+23 -20 metaprl/support/shell/proof_edit.mli
+56 -48 metaprl/support/shell/shell.ml
+3 -1 metaprl/support/shell/shell_browser.ml
+2 -2 metaprl/support/shell/shell_java.ml
+20 -12 metaprl/support/shell/shell_package.ml
+19 -11 metaprl/support/shell/shell_root.ml
+17 -27 metaprl/support/shell/shell_rule.ml
+26 -20 metaprl/support/shell/shell_sig.mlz
+21 -13 metaprl/support/shell/shell_state.ml
+2 -1 metaprl/support/shell/shell_state.mli
+1 -1 metaprl/support/tactics/auto_tactic.ml
+1 -1 metaprl/support/tactics/dtactic.ml
+2 -1 metaprl/support/tactics/simp_typeinf.ml
+2 -1 metaprl/support/tactics/tactic_cache.ml
+1 -1 metaprl/support/tactics/top_conversionals.ml
+2 -1 metaprl/support/tactics/typeinf.ml
+2 -1 metaprl/support/tactics/var.ml
+1 -1 metaprl/tactics/ensemble/appl_closure.ml
+2 -2 metaprl/tactics/ensemble/appl_outboard_client.ml
+2 -2 metaprl/tactics/ensemble/appl_outboard_server.ml
+1 -1 metaprl/tactics/ensemble/ensemble_queue.ml
+1 -1 metaprl/tactics/ensemble/remote_ensemble.ml
+1 -2 metaprl/tactics/ensemble/remote_monitor.ml
+1 -1 metaprl/tactics/ensemble/thread_refiner.ml
+1 -0 metaprl/tactics/proof/conversionals_boot.ml
+1 -1 metaprl/tactics/proof/exn_boot.ml
+9 -15 metaprl/tactics/proof/proof_boot.ml
+1 -1 metaprl/tactics/proof/proof_convert.ml
+1 -0 metaprl/tactics/proof/proof_term_boot.ml
+1 -1 metaprl/tactics/proof/rewrite_boot.ml
+1 -0 metaprl/tactics/proof/sequent_boot.ml
+4 -3 metaprl/tactics/proof/tactic_boot.ml
+4 -4 metaprl/tactics/proof/tactic_boot_sig.ml
+1 -0 metaprl/tactics/proof/tacticals_boot.ml
+5 -18 metaprl/theories/czf/czf_itt_abel_group.ml
+1 -0 metaprl/theories/czf/czf_itt_all.ml
+1 -0 metaprl/theories/czf/czf_itt_and.ml
+6 -20 metaprl/theories/czf/czf_itt_axioms.ml
+7 -21 metaprl/theories/czf/czf_itt_coset.ml
+9 -25 metaprl/theories/czf/czf_itt_cyclic_group.ml
+8 -23 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+8 -25 metaprl/theories/czf/czf_itt_dall.ml
+8 -25 metaprl/theories/czf/czf_itt_dexists.ml
+4 -14 metaprl/theories/czf/czf_itt_empty.ml
+1 -0 metaprl/theories/czf/czf_itt_equiv.ml
+1 -0 metaprl/theories/czf/czf_itt_exists.ml
+1 -0 metaprl/theories/czf/czf_itt_false.ml
+1 -0 metaprl/theories/czf/czf_itt_group.ml
+6 -19 metaprl/theories/czf/czf_itt_group_bvd.ml
+7 -22 metaprl/theories/czf/czf_itt_group_power.ml
+14 -39 metaprl/theories/czf/czf_itt_hom.ml
+1 -0 metaprl/theories/czf/czf_itt_implies.ml
+6 -20 metaprl/theories/czf/czf_itt_inv_image.ml
+9 -24 metaprl/theories/czf/czf_itt_isect.ml
+5 -16 metaprl/theories/czf/czf_itt_iso.ml
+10 -22 metaprl/theories/czf/czf_itt_ker.ml
+1 -0 metaprl/theories/czf/czf_itt_kleingroup.ml
+6 -20 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+1 -0 metaprl/theories/czf/czf_itt_or.ml
+6 -19 metaprl/theories/czf/czf_itt_sall.ml
+9 -26 metaprl/theories/czf/czf_itt_sep.ml
+1 -0 metaprl/theories/czf/czf_itt_set.ml
+7 -22 metaprl/theories/czf/czf_itt_set_bvd.ml
+1 -0 metaprl/theories/czf/czf_itt_set_ind.ml
+7 -11 metaprl/theories/czf/czf_itt_setdiff.ml
+6 -19 metaprl/theories/czf/czf_itt_sexists.ml
+6 -18 metaprl/theories/czf/czf_itt_singleton.ml
+8 -24 metaprl/theories/czf/czf_itt_subgroup.ml
+1 -0 metaprl/theories/czf/czf_itt_true.ml
+11 -29 metaprl/theories/czf/czf_itt_union.ml
+1 -2 metaprl/theories/experimental/compile/m_post_parsing.ml
+3 -2 metaprl/theories/experimental/compile/m_ra_live.ml
+11 -11 metaprl/theories/experimental/compile/m_ra_main.ml
+2 -2 metaprl/theories/experimental/compile/m_ra_state.ml
+2 -2 metaprl/theories/experimental/compile/m_ra_state.mli
+2 -2 metaprl/theories/experimental/compile/m_ra_type.mlz
+1 -2 metaprl/theories/experimental/compile/m_standardize.ml
+1 -1 metaprl/theories/experimental/compile/m_util.ml
+34 -23 metaprl/theories/experimental/compile/m_x86_backend.ml
+1 -1 metaprl/theories/experimental/compile/m_x86_backend.mli
+1 -1 metaprl/theories/experimental/compile/m_x86_coalesce.ml
+2 -3 metaprl/theories/experimental/compile/m_x86_regalloc.ml
+1 -1 metaprl/theories/experimental/unity/unity_util.ml
+1 -0 metaprl/theories/itt/ctt_markov.ml
+1 -0 metaprl/theories/itt/itt_atom.ml
+11 -11 metaprl/theories/itt/itt_bintree.ml
+1 -0 metaprl/theories/itt/itt_cyclic_group.ml
+6 -6 metaprl/theories/itt/itt_datatree.ml
+7 -22 metaprl/theories/itt/itt_decidable.ml
+1 -0 metaprl/theories/itt/itt_dfun.ml
+1 -0 metaprl/theories/itt/itt_disect.ml
+2 -1 metaprl/theories/itt/itt_dprod.ml
+1 -1 metaprl/theories/itt/itt_dprod_imp.ml
+1 -1 metaprl/theories/itt/itt_equal.ml
+1 -0 metaprl/theories/itt/itt_ext_equal.ml
+1 -0 metaprl/theories/itt/itt_field2.ml
+1 -0 metaprl/theories/itt/itt_field_e.ml
+1 -1 metaprl/theories/itt/itt_fset.ml
+1 -0 metaprl/theories/itt/itt_fun.ml
+1 -0 metaprl/theories/itt/itt_group.ml
+1 -0 metaprl/theories/itt/itt_grouplikeobj.ml
+3 -2 metaprl/theories/itt/itt_int_arith.ml
+3 -2 metaprl/theories/itt/itt_int_base.ml
+1 -0 metaprl/theories/itt/itt_int_ext.ml
+1 -0 metaprl/theories/itt/itt_intdomain.ml
+1 -0 metaprl/theories/itt/itt_intdomain_e.ml
+1 -0 metaprl/theories/itt/itt_isect.ml
+1 -0 metaprl/theories/itt/itt_list.ml
+1 -1 metaprl/theories/itt/itt_logic.ml
+1 -0 metaprl/theories/itt/itt_nequal.ml
+1 -0 metaprl/theories/itt/itt_order.ml
+1 -0 metaprl/theories/itt/itt_pointwise.ml
+3 -2 metaprl/theories/itt/itt_pointwise2.ml
+1 -0 metaprl/theories/itt/itt_poly.ml
+2 -1 metaprl/theories/itt/itt_prec.ml
+9 -23 metaprl/theories/itt/itt_prod.ml
+1 -1 metaprl/theories/itt/itt_prop_decide.ml
+1 -0 metaprl/theories/itt/itt_quotient.ml
+1 -0 metaprl/theories/itt/itt_quotient_group.ml
+1 -0 metaprl/theories/itt/itt_rat.ml
+13 -13 metaprl/theories/itt/itt_rbtree.ml
+1 -0 metaprl/theories/itt/itt_record.ml
+1 -0 metaprl/theories/itt/itt_record0.ml
+2 -1 metaprl/theories/itt/itt_rfun.ml
+1 -0 metaprl/theories/itt/itt_ring2.ml
+1 -0 metaprl/theories/itt/itt_ring_e.ml
+1 -0 metaprl/theories/itt/itt_ring_uce.ml
+1 -0 metaprl/theories/itt/itt_set.ml
+6 -17 metaprl/theories/itt/itt_singleton.ml
+3 -3 metaprl/theories/itt/itt_sortedtree.ml
+1 -0 metaprl/theories/itt/itt_squash.ml
+1 -0 metaprl/theories/itt/itt_squiggle.ml
+2 -1 metaprl/theories/itt/itt_srec.ml
+1 -0 metaprl/theories/itt/itt_struct.ml
+1 -0 metaprl/theories/itt/itt_struct2.ml
+1 -0 metaprl/theories/itt/itt_struct3.ml
+1 -0 metaprl/theories/itt/itt_subset.ml
+12 -27 metaprl/theories/itt/itt_subset2.ml
+1 -0 metaprl/theories/itt/itt_subtype.ml
+2 -1 metaprl/theories/itt/itt_supinf.ml
+2 -1 metaprl/theories/itt/itt_union.ml
+8 -20 metaprl/theories/itt/itt_unit.ml
+1 -0 metaprl/theories/itt/itt_unitring.ml
+1 -0 metaprl/theories/itt/itt_void.ml
+1 -2 metaprl/theories/kat/support_algebra.ml
+5 -5 metaprl/theories/lf/main.ml
+1 -1 metaprl/theories/mesa/ma_decidable__equality.ml
+3 -12 metaprl/theories/ocaml_doc/ocaml_doc_expr1.ml
+5 -13 metaprl/theories/ocaml_doc/ocaml_doc_io1.ml
+14 -22 metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_logic.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+5 -5 metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+1 -1 metaprl/theories/tptp/tptp_cache.ml
+12 -11 metaprl/theories/tptp/tptp_lex.mll
+1 -2 metaprl/theories/tptp/tptp_load.ml
+2 -1 metaprl/theories/tptp/tptp_prove.ml
+1 -1 metaprl/util/unicode.ml