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

Hi Makarius,

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 â
   where_it_makes_sense_to_use â several_lines) type_constructor"
  "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 â
  where_it_makes_sense_to_use â several_lines) type_constructor,"
    "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

I haven't tried this changes yet and I cannot tell from a quick look at the sources what they do. I hope that outer syntax now ignores the indentation of inner syntax (which was not the case in Isabelle2016-1-RC2).

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.
Indeed, one could argue forever whether

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


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

is better. I prefer the former because it saves to spaces of indentation, so I can stick two more characters onto a line. But that's not a strong argument.

What I found confusing was that the level of indentation depends on whether "where" is on a line of its own or not. In Isabelle2016-1-RC2, I get the following indentation behaviour:

definition bar :: "nat â nat" where
  "bar = id"

definition bar :: "nat â nat"
    "bar = id"

This does *not* make sense to me and I find it quite annoying. Especially if the right hand side spans several lines. Then, when I change the type, say because I have to add another parameter, and put the "where" quasi-command on a new line, I have to adjust the indentation of the whole right hand side. For me, it's OK if we indent definitions by 4 spaces, but it's not OK if the indentation depends on whether the "where" is on the same line or not.

By the way, the same applies to "obtain" inside Isar proofs. Here's such a silly example of an indentation produced by C-c C-i:

notepad begin
  obtain n :: nat where "n = n"
    and "n = n" sorry

  obtain n :: nat
    where "n = n"
      and "n = n" sorry

I hope that your changeset above addresses these inconsistencies.


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