Re: [isabelle] [Isabelle2016-1-RC2] Experience with auto-indentation



On 21/11/16 16:58, Andreas Lochbihler wrote:
> 
> A follow-up on this issue. I've now observed a similarly wrong
> indentation with context blocks:
> 
> context<RET>assumes "True"<RET>and "True"<RET>begin
> 
> yields
> 
> context
>   assumes "True"
>   and "True"
> begin
> 
> rather than
> 
> context
>   assumes "True"
>     and "True"
> begin
> 
> This is on a freshly installed Isabelle2016-1-RC2 in an empty theory.

I have refined that in
https://bitbucket.org/isabelle_project/isabelle-release/commits/e61de633a3eddc6

This makes indentation more uniform and predictable, but produces more
spaces in intermediate situations. The WhiteSpace plugin of jEdit helps
to remove trailing space systematically, e.g. on buffer save.

I reckon there will be one more release candidate (RC5), before final
lift-off. If you want to test it right now, you need to use the above
repository version: http://isabelle.in.tum.de/devel is already back to
post-release mode and now delivers isabelle-dev snapshots instead of
release snapshots.


	Makarius





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