On 1 Apr 2013, at 01:21, Seth Lastname wrote:
Note 2 says, "If the first token after a 'where' (say) is not indented more than the enclosing layout context, then the block must be empty, so empty braces are inserted."
It seems that, in Note 2, the "first token" necessarily refers to a lexeme other than '{' (else it would not make sense),
Correct.
in which case a '{n}' token will have been inserted after 'where' (in the example given in the note), yielding a nested context which is "not indented more than the enclosing layout context",
Yes, a "{n}" token has been inserted after the "where".
No, it does not yield an incorrectly nested context, because L is the function that decides whether to add to the context.
Looking only at the three equations for L that deal with the pseudo-token "{n}", including their side conditions, we see:
L ({n} : ts) (m : ms) = { : (L ts (n : m : ms)) if n > m (Note 1)
L ({n} : ts) [] = { : (L ts [n]) if n > 0 (Note 1)
L ({n} : ts) ms = { : } : (L (< n >: ts) ms) (Note 2)
So, the third clause is triggered either when the nested-context stack (ms) is empty and n is zero or negative; or when the context stack is non-empty and n