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.
> 
> 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.)


	Makarius


theory Scratch
  imports Main
begin

lemma
  assumes "True"
    and "True"
  shows "True"
  ..

end


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