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

and

x y
: z

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

P.


> -Jason
>
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to