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



Hi Makarius,

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. If necessary, I can also try to shoot a short video of my screen.

Andreas

On 21/11/16 16:27, Andreas Lochbihler wrote:
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.