Re: [isabelle] [Isabelle2016-1-RC2] Experience with auto-indentation
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.
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
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