@@ -48,13 +48,13 @@ This is added to the ``TokenMap`` like this:
4848 (operator, \x => Operator x),
4949 (is '(' ,\x => OParen),
5050 (is ')' ,\x => CParen),
51− (space, Comment),
51+ (spaces, Comment),
5252 (comment, Comment)]
5353
5454As you can see, the comment is defined like a single line Idris comment,
5555it starts with ``--`` and continues for the remainder of the line.
5656
57−We don't need to define ``space`` because it is already defined in
57+We don't need to define ``spaces`` because it is already defined in
5858: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr
5959like this:
6060
@@ -75,11 +75,6 @@ Whitespace and Comments in Parser
7575
7676Now that there are ``Comment`` tokens the parser needs to be able to handle them.
7777
78−So far we don't have any syntax that requires spaces to be significant so we
79−need to define the grammar so that it will parse with, or without, spaces.
80−This needs to be done in a systematic way, here I have defined the grammar so
81−that there is an optional space to the right of every atom or operator:
82−
8378.. code-block:: idris
8479
8580 commentSpace : Rule Integer
@@ -87,6 +82,11 @@ that there is an optional space to the right of every atom or operator:
8782 Comment s => Just 0
8883 _ => Nothing)
8984
85+So far we don't have any syntax that requires spaces to be significant so we
86+need to define the grammar so that it will parse with, or without, spaces.
87+This needs to be done in a systematic way, here I have defined the grammar so
88+that there is an optional space to the right of every atom or operator:
89+
9090.. code-block:: idris
9191
9292 partial
@@ -122,6 +122,24 @@ that there is an optional space to the right of every atom or operator:
122122
123123 expr = expr3 <|> exprAdd
124124
125+Defining Block Structure using Indents
126+--------------------------------------
127+
128+Many languages such as Python, Haskell and Idris use indents to delimit
129+the block structure of the language.
130+
131+We can see how Idris2 does it here
132+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
133+
134+.. code-block:: idris
135+
136+ export
137+ IndentInfo : Type
138+ IndentInfo = Int
139+
140+ export
141+ init : IndentInfo
142+ init = 0
125143
126144
127145