Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-17 23:09:20 -0700 (Thu, 17 Apr 2003)
Revision: 4449
Log message:

      - More precise error messages when parsing comments:
      a) The "undeclared opname" errors now give the address of the actual opname,
      not of the whole comment the opname is in
      b) The error messages that happen when parsing a << >> quotation inside
      <:doc< >> quotation now give the actual address, not the address relative to
      the << beginning. These messages currently give the address a few symbols off,
      not sure why.
      
      - The << >> quotations inside <:doc< >> are now always assumed to imply the
      math mode. I.e. <:doc< ... << ... >> ... >> will get parsed the same as
      <:doc< ... $<< ... >>$ ... >> (unless, of course, the << ... >> was already
      inside the math mode).
      
      - Started getting rid of unneeded math_ terms in itt_comment.
      
      - Made the display form for esquash nicer (uses the actual double-bracket
      symbols instead of [[ ]] which can be confused with squash{squash{ }}).
      
      - The display form for assert is up arrow (it used to be inconsistent -
      up in some places, down in some), same as in Nuprl (in Nuprl, the
      downarrow is a display form for squash).
      
      - Fixed the prl mode dform for sube.
      
      - Spelling fixes
      

Changes  Path
+13 -10 metaprl/filter/filter/term_grammar.ml
+1 -0 metaprl/lib/words
+7 -5 metaprl/mllib/comment_parse.mli
+25 -13 metaprl/mllib/comment_parse.mll
+1 -1 metaprl/theories/base/base_rewrite.ml
+2 -2 metaprl/theories/czf/czf_itt_union.ml
+1 -1 metaprl/theories/experimental/compile/m_doc_comment.ml
+5 -5 metaprl/theories/experimental/compile/m_doc_ir.ml
+4 -4 metaprl/theories/experimental/compile/m_doc_x86_asm.ml
+15 -21 metaprl/theories/experimental/compile/m_x86_codegen.ml
+1 -1 metaprl/theories/fir/mfir_int_set.ml
+27 -27 metaprl/theories/fir/mfir_tr_atom.ml
+6 -6 metaprl/theories/fir/mfir_tr_base.ml
+12 -12 metaprl/theories/fir/mfir_tr_exp.ml
+4 -4 metaprl/theories/fir/mfir_tr_store.ml
+8 -8 metaprl/theories/fir/mfir_tr_types.ml
+3 -3 metaprl/theories/fir/mfir_util.ml
+5 -6 metaprl/theories/itt/itt_bool.ml
+0 -18 metaprl/theories/itt/itt_comment.ml
+0 -2 metaprl/theories/itt/itt_comment.mli
+1 -1 metaprl/theories/itt/itt_dprod.ml
+11 -11 metaprl/theories/itt/itt_esquash.ml
+1 -1 metaprl/theories/itt/itt_group.ml
+1 -1 metaprl/theories/itt/itt_list2.ml
+10 -10 metaprl/theories/itt/itt_logic.ml
+11 -11 metaprl/theories/itt/itt_record_exm.ml
+1 -1 metaprl/theories/itt/itt_relation_str.ml
+2 -2 metaprl/theories/itt/itt_rfun.ml
+20 -20 metaprl/theories/itt/itt_set_str.ml
+1 -1 metaprl/theories/itt/itt_singleton.ml
+6 -6 metaprl/theories/itt/itt_squash.ml
+6 -6 metaprl/theories/itt/itt_squiggle.ml
+1 -1 metaprl/theories/itt/itt_struct.ml
+4 -4 metaprl/theories/itt/itt_struct2.ml
+18 -18 metaprl/theories/itt/itt_subset.ml
+4 -4 metaprl/theories/itt/itt_subset2.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+5 -5 metaprl/theories/itt/itt_union.ml
+3 -3 metaprl/theories/tactic/comment.ml
+12 -1 metaprl/theories/tactic/nuprl_font.ml
+1 -16 metaprl/theories/tactic/nuprl_font.mli