I did not see bugs about these pre-existing.  I have created #473 and #474.
 I may have run into other bugs, but these are the two that bite me
repeatedly, to the extent that I change my code to work around them.


On Fri, Jul 5, 2013 at 11:07 AM, Jason Gross <jasongro...@gmail.com> wrote:

> Hi,
>  Except #466 are there other bugs on indentation? I don't see them.
> I have had a number of indentation issues with PG.  I will go check the
> bug list and file new tickets if they are not there.  In short, my biggest
> issues have been with "Arguments foo /." (adding a space after the "/"
> fixes it) and with "{ foo : T & bar }" with a newline before/after the "&".
>  I will get back to you soon with either newly reported bugs or a message
> that these have already been reported and fixed.
> Additionally, I would be curious to know if it is intentional that the ":"
> in
> {{
> Definition foo
> : T.
> }}
> is not indented beyond the [Definition].
> -Jason
ProofGeneral-devel mailing list

Reply via email to