Fix #1767

The `if then else` syntax expects a block for the `then` and `else`
parts. Before this patch, the token `InterpEnd` was not a valid
follow up token to end a block. This adds `InterpEnd` as a closing
token for blocks, allowing `if then else` in interpolation slices
without additional parens.

Author: andrevidela

src/Parser/Rule/Source.idr

@@ -400,6 +400,7 @@ isTerminator (Keyword "in") = True
 isTerminator (Keyword "then") = True
 isTerminator (Keyword "else") = True
 isTerminator (Keyword "where") = True
+isTerminator InterpEnd = True
 isTerminator EndInput = True
 isTerminator _ = False
 

tests/Main.idr

@@ -41,7 +41,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic046", "basic047",             "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
-       "basic061"]
+       "basic061", "interpolation001"]
 
 idrisTestsCoverage : TestPool
 idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing

tests/idris2/interpolation001/IfThenElse.idr

@@ -0,0 +1,2 @@
+ifthenelse : String
+ifthenelse = "\{ if True then "a" else "b" }"

tests/idris2/interpolation001/expected

@@ -0,0 +1 @@
+1/1: Building IfThenElse (IfThenElse.idr)

tests/idris2/interpolation001/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check --alt-error-count 10 IfThenElse.idr
+