[ doc #354 ] lbnf.rst: stacking layout keywords

docs/lbnf.rst

@@ -869,6 +869,87 @@ first column, and the resolver adds a semicolon after every paragraph
 whose first token is at this position. No curly brackets are added. The
 Alfa file above is an example of this, with two such semicolons added.
 
+Stacking layout keywords
+------------------------
+
+Since version 2.9.2, the layout processor supports stacking of layout
+keywords on the same line.  Consider the following fragment of an
+Agda-ish grammar::
+
+    Module.   Decl ::= "module" Ident "where" "{" [Decl] "}" ;
+    Private.  Decl ::= "private" "{" [Decl] "}" ;
+    TypeSig.  Decl ::= Ident ":" Ident ;
+
+    separator Decl ";" ;
+
+    layout "where", "private" ;
+
+This grammar allows us to define simple Agda modules that contain a
+list of declarations, each of which can be a module, a private block
+or a type signature.  Lists of declarations are enclosed in braces
+and separated by semicolons, and introduced by the layout keywords
+``where`` and ``private``.
+
+We may want to define a private module, and instead of two subsequent indentations::
+
+    private
+      module M where
+        A : Set
+
+we wish to stack the two layout introductions on a single line::
+
+    private module M where
+      A : Set
+
+This is not supported by the layout logic up to BNFC 2.9.1, as we
+would fix the layout column for the ``private`` block to column 8, the
+column of token ``module``.  The token ``A`` following the next layout
+keyword ``where`` lives at column 2 which is below 8, thus, the
+``private`` block would be closed here.  But with ``private``
+closing, the inner block ``module M where`` also needs to close, and
+then the declaration ``A : Set`` is simply misindented.  Thus, this
+gives a parse error with BNFC 2.9.1.
+
+The layout processor produced by BNFC 2.9.2 instead marks the layout
+column 8 of the ``private`` block as *tentative* since the token
+``module`` following the layout keyword ``private`` is on the same
+line.  On the contrary, the layout column 2 of the ``module`` block is
+*definitive* since the token ``A`` following the layout keyword
+``where`` is at a later line.  When checking whether a new layout
+column is valid, tentative layout columns get ignored, thus it is only
+checked that 2 > 0, not that 2 > 8.  When at some
+point the ``module`` block will be closed because we encounter a token
+indented less than 2, the ``private`` block will be closed as well
+since its indentation column 8 is also greated than the indentation of
+the encountered token.
+
+In general, when encountering a new line, we switch the top layout
+columns to *definitive* if they are still *tentative*.  For instance,
+consider the following situation::
+
+    private module M where A : Set
+            module N where
+      Bad : Set
+
+At the end of the first line, we have two tentative layout columns, 8
+(column of ``module``) and 23 (column of ``A``).  Since now we have no
+pending layout keyword left in this line, we switch the layout columns
+to *definitive* when we see the next token ``module`` on a new line.
+The first module closes here, leaving us with definitive layout
+column 8.  This prevents that we assign to the subsequent block
+``module N`` with layout keyword ``where`` the column 2 (token
+``Bad``).  Instead, this block gets a default column, 8+1.  When
+processing token ``Bad`` both blocks get closed since 2 < 8 and 2 < 8+1.
+But then ``Bad`` is
+misindented, yielding the expected parse error.
+
+The changes introduced for *stacking layout keywords* are backwards
+compatible in the following sense: A layout-aware parser generated by
+BNFC 2.9.2 accepts all texts that were soundly accepted by the
+respective parser generated by BNFC 2.9.1 and before.  Further, the
+same syntax trees are generated for these accepted texts.
+
+
 .. _leftrec:
 
 An optimization: left-recursive lists
@@ -983,8 +1064,8 @@ Comments
 | Single-line comments begin with ``--``.
 | Multiple-line comments (aka *block comments*) are enclosed between ``{-`` and ``-}``.
 
-The syntactic structure of BNF
-==============================
+The syntactic structure of LBNF
+===============================
 
 Non-terminals are enclosed between ``<`` and ``>``.
 The symbols ``::=`` (production), ``|`` (union) and ``ε`` (empty rule)

source/CHANGELOG.md

@@ -5,6 +5,7 @@ Andreas Abel <andreas.abel@gu.se>  (unreleased)
 ## Major improvements
 
 * Haskell: layout keywords can now be stacked on the same line [#354]
+  See https://bnfc.readthedocs.io/en/latest/lbnf.html#stacking-layout-keywords
 * C/C++ backends now create reentrant parsers [#349]
 
 ## Bug fixes and small improvements