Thanks!

I have just remembered some other indentation issues I've run into, and
created #475-#478 (though #477 is technically highlighting, not
indentation).

-Jason

On Monday, July 8, 2013, Pierre Courtieu wrote:

> Hi, thanks for the bug reports.
>
>
> 2013/7/5 Jason Gross <jasongro...@gmail.com <javascript:_e({}, 'cvml',
> '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