Merge pull request #3361 from Matthew-Mosior/issue-2766-hint-not-listed-as-a-pragma

`%hint` not listed as a pragma
This commit is contained in:
André Videla 2024-07-31 16:26:29 +01:00 committed by GitHub
commit b1fff6f919
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 8 additions and 2 deletions

View File

@ -16,6 +16,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
installed will be ignored by the compiler when it tries to use that library as
a dependency for some other package.
* The `idris2 --help pragma` command now outputs the `%hint` pragma.
* The `idris2 --init` command now ensures that package names are
valid Idris2 identifiers.

View File

@ -6,7 +6,8 @@ import Data.String
public export
data KwPragma
= KwHide
= KwHint
| KwHide
| KwUnhide
| KwLogging
| KwAutoLazy
@ -76,6 +77,7 @@ Show PragmaArg where
export
pragmaArgs : KwPragma -> List PragmaArg
pragmaArgs KwHint = []
pragmaArgs KwHide = [AName "nm"]
pragmaArgs KwUnhide = [AName "nm"]
pragmaArgs KwLogging = [AnOptionalLoggingTopic, ANat]
@ -101,6 +103,7 @@ pragmaArgs KwSearchTimeOut = [ANat]
export
Show KwPragma where
show kw = case kw of
KwHint => "%hint"
KwHide => "%hide"
KwUnhide => "%unhide"
KwLogging => "%logging"
@ -126,7 +129,8 @@ Show KwPragma where
export
allPragmas : List KwPragma
allPragmas =
[ KwHide
[ KwHint
, KwHide
, KwUnhide
, KwLogging
, KwAutoLazy