3a69398 · Idris-dev · git.iko.soy

src/Idris/Parser.hs+6−2

@@ -2400,10 +2400,14 @@ directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- strin

2400 Left lib -> addIBC (IBCDyLib (lib_name lib))

2401 Right msg ->

2402 fail $ msg)])

2403− <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";

2403+ <|> try (do lchar '%'; reserved "language"; ext <- pLangExt;

2404− return [PDirective (addLangExt TypeProviders)])

2404+ return [PDirective (addLangExt ext)])

2405 <?> "directive"

2406

2407+pLangExt :: IdrisParser LanguageExt

2408+pLangExt = (reserved "TypeProviders" >> return TypeProviders)

2409+ <|> (reserved "ErrorReflection" >> return ErrorReflection)

2410+

2407{- | Parses a totality

2411{- | Parses a totality

2408Totality ::= 'partial' | 'total'

2412Totality ::= 'partial' | 'total'

2409-}

2413-}

test/test031/expectednew file

No changes to the content.

test/test031/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ test031.idr -o test031

3+./test031

4+rm -f test031 *.ibc

test/test031/test031.idrnew file+8

@@ -0,0 +1,8 @@

1+module Main

2+

3+-- Test enabling the ErrorReflection extension

4+

5+%language ErrorReflection

6+

7+main : IO ()

8+main = return ()