Re: [isabelle] Indentation quirks after oops



Dear all,

just to revive this old thread, I came upon this odd indentation after
"oops" again today (using Isabelle2018). In my case I was surprised
about the indentation of "term" after "oops".

  lemma "A ⟹ B"
    oops

    term C

cheers

chris

On 11/14/17 2:51 PM, Makarius wrote:
> On 01/11/17 13:06, Andreas Lochbihler wrote:
>>
>> In Isabelle2017, the auto-indentation feature feels weird when there is
>> I abort a proof with oops.
> 
>> lemma False
>> proof -
>>   have False
>>     oops
>>
>>     section bar
> 
>> Am I doing something wrong here or is this indentation behaviour just
>> something that could be improved in future releases?
> 
> The 'oops' command is always apt to odd special cases. I don't know a
> better way for Isabelle2017. It is something to be improved eventually.
> 
> BTW, commands like 'text' or 'section' were once more restricted in
> there occurrences. Now they can occur anywhere and don't enforce a
> particular indentation on there own, in contrast to theory commands like
> 'definition' or 'theorem'.
> 
> 
> 	Makarius
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.