Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-09 00:30:13 -0700 (Wed, 09 Apr 2003)
Revision: 4406
Log message:

      Comment parsing:
      - now it does not make sence to consider "*" symbol after whitespace
      at the beginning of a new line as a whitespace.
      
      Comment prl display:
      - "@begin[doc]", "@end[doc]", "(*" and "*)" will now be displayed bold
      - Multi-line comment will now be correctly terminated by " *)" on the last line,
      and not " *  *)"
      
      mpxterm scripts:
      - mpxterm will now use the same font for normal and bold display (since the
      bold version of the fond does not have tha "vdash" symbol).
      - both mpxterm and mpxterm-large will now display bold as brown.
      

Changes	Path
+0 -2	metaprl/Makefile
+2 -1	metaprl/editor/ml/mpxterm
+1 -1	metaprl/editor/ml/mpxterm-large
+1 -2	metaprl/mllib/comment_parse.mll
+4 -4	metaprl/theories/tactic/comment.ml