Hi, thanks for the bug reports.

2013/7/5 Jason Gross <jasongro...@gmail.com>

> 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)

Fixed. Any combination of symbols finishing by a dot (except "..") is now
considered a command end.

  and with "{ foo : T & bar }" with a newline before/after the "&".

fixed too, but I don't have generic way to deal with all operators
including those defined by the user.

>  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].

Good question. I tend to consider this normal because ":" is an binary
operator like "+". Therefore

x y
+ z


x y
: z

are correct. But I must admit it is a bit unsatisfying...


> -Jason
ProofGeneral-devel mailing list

Reply via email to