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

On 11/11/16 16:07, Andreas Lochbihler wrote:
> 2. The keyword "where" in definitions is indented according to the
> indentation of the type when the type spans several lines. For example,
> definition foo :: "this_is_a_very â
>   (long_type,
>    where_it_makes_sense_to_use â several_lines) type_constructor"
>    where
>   "foo = undefined"
> Here, "where" is indented on space too far (three instead of two),
> because the last line of the type is indented by one (which I find
> desireable, because it emphasizes that the return type of the function
> goes on).
> What is the point of aligning minor keywords like "where" with the
> previous line of inner syntax? IMO "where" belongs to the outer syntax
> of "definition" and should therefore ignore any alignment of inner syntax.
> Of course, I can manually delete the space before "where", but whenever
> I hit <RET> again on that line, it will insert it again. :-(
> 3. Reformatting destroys all semantic indentation of inner syntax. For
> example, in the example of 2., when I mark the whole definition and
> press C-C C-i, I get
> definition foo :: "this_is_a_very â
>   (long_type,
>   where_it_makes_sense_to_use â several_lines) type_constructor,"
>   where
>     "foo = undefined"
> This seems wrong for two reasons: First, it has destroyed the formatting
> of the type. Second, the specification equation is now indented by 4
> spaces. Why should we indent specifications by 4 spaces? The position of
> the "where" (on the line of the type vs. on a new line) should not
> affect the indentation, but apparently it does. Is there a good reason
> for this?

There are actually two different effects seen in both 2. and 3.:

  (a) inner syntax vs. outer syntax
  (b) indendation of 'where'

Inner syntax is not taken into account in indentation right now: it is
far to complex and PIDE markup for its structure is mostly missing. To
clarify the non-observance of inner syntax further, I have made two
small changes in

The 'where' keyword is different. It belongs to a new category of "quasi
commands"; other examples are 'imports', 'fixes', 'assumes', 'shows',
'obtains'. These keywords are indented like a secondary command that is
nested inside the main command. This explains the 4 instead of 2 spaces

definition foo
    "foo x = x"

Here is definition with more clauses. It shows how everything fits
nicely together:

fun bar :: "nat â nat"
    "bar 0 = 0"
  | "bar (Suc n) = n"

This indentation of 'imports', 'where', '|' is a change of what I have
considered canonical indentation over many years. But there was no
particular reason for the former format. The reason for the new one is
more uniformity: fewer rules and special cases are required to specify
how indentation works.


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