Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 22:20:25 -0700 (Thu, 24 Apr 2003)
Revision: 4491
Log message:

      - Rformat: Added a notion of "tagged" boxes that need to be closed and re-opened
      on line break. The ensuremath macro is now implemented as a tagged box
      - Updated display forms so that the new dform for "declare" does not create
      problems of helper terms (such as those in the Comment theory).
      

Changes  Path
+1 -1 metaprl/filter/base/filter_cache_fun.ml
+5 -0 metaprl/refiner/reflib/dform.ml
+71 -79 metaprl/refiner/reflib/rformat.ml
+2 -0 metaprl/refiner/reflib/rformat.mli
+105 -47 metaprl/theories/tactic/comment.ml
+3 -3 metaprl/theories/tactic/nuprl_font.ml
+1 -1 metaprl/theories/tactic/summary.ml
+6 -6 texinputs/metaprl.tex