Re: [isabelle] [Isabelle2016-1-RC2] Experience with auto-indentation
On 11/11/16 16:07, Andreas Lochbihler wrote:
> 1. Indentation does not work properly if I write a lemma statement from
> top to bottom.
> For example, put the curser at the beginning of a line in a theory and
> type the following (<RET> denotes the return key which is bound to
> "Newline with indentation of Isabelle keywords"):
> lemma<RET>assumes "True"<RET>and "True"<RET>shows "True"<RET>
> Here is what the automatic indentation produces in the editor, which is
> clearly not what I want and would have expected. So I have to go over it
> again and adjust the indentation. This requires more typing than without
> automatic indentation.
> assumes "True"
> and "True"
> shows "True"
This looks strange, but it might be just the mailer messing up the
indentation. I am including my own experiment in Scratch.thy, which
looks fine to me.
(This is Isabelle2016-1-RC2 with clean defaults.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and