@@ -190,14 +190,61 @@ We can see how Idris2 does it here
190 init : IndentInfo
190 init : IndentInfo
196+So far, the parser will return a successful result even if the full input
197+is not consumed. To ensure that the top level syntax is fully matched we
198+add a ``EndInput`` token to indicate the last token.
200+``EndInput`` is added to the other tokens like this:
202+.. code-block:: idris
204+ data ExpressionToken = Number Integer
211+A rule to consume this token is added:
213+.. code-block:: idris
216+ eoi = terminal (\x => case tok x of
220+Instead of using ``expr`` at the top level of the syntax we can now define
221+``exprFull`` as shown here. This will make sure that only when ``EndInput``
222+is consumed will the parse be successful:
224+.. code-block:: idris
226+ exprFull : Rule Integer
227+ exprFull = expr <* eoi
229+The following code makes sure ``EndInput`` is added to the end of the token
232+.. code-block:: idris
234+ processWhitespace : (List (TokenData ExpressionToken), Int, Int, String)
235+ -> (List (TokenData ExpressionToken), Int, Int, String)
236+ processWhitespace (x,l,c,s) = ((filter notComment x)++
237+ [MkToken l c EndInput],l,c,s) where
238+ notComment : TokenData ExpressionToken -> Bool
239+ notComment t = case tok t of
243+All we have to do now is use ``exprFull`` instead of ``expr``:
245+.. code-block:: idris
247+ calc : String -> Either (ParseError (TokenData ExpressionToken))
248+ (Integer, List (TokenData ExpressionToken))
249+ calc s = parse exprFull (fst (processWhitespace (lex expressionTokens s)))