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



Hi Makarius,

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.

lemma
  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.)
When I wrote my e-mail 1.5 weeks ago, I really got the indentation as shown in the quote above (with show starting in the first column). When I tried today again, I was not able to reproduce this behaviour. I get the same indentation as you got. Strange.

Andreas




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