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