All fixed, except that Instance cannot be indented by default because
it is impossible to know by syntax that it starts a goal or not. The
user should put Proof (once) when starting the proof or better: put
curly brackets around each subgoal.

P.

2013/7/10 Jason Gross <jasongro...@gmail.com>:
> 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>
>>>
>>> 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