Skip to content

Commit

Permalink
Adding files to address issue #2766.
Browse files Browse the repository at this point in the history
  • Loading branch information
Matthew-Mosior committed Jul 26, 2024
1 parent 91d0eb3 commit d99a48b
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 2 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

### Building/Packaging changes

* The Nix flake's `buildIdris` function now returns a set with `executable` and
Expand Down
8 changes: 6 additions & 2 deletions src/Idris/Syntax/Pragmas.idr
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@ import Data.String

public export
data KwPragma
= KwHide
= KwHint
| KwHide
| KwUnhide
| KwLogging
| KwAutoLazy
Expand Down Expand Up @@ -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]
Expand All @@ -101,6 +103,7 @@ pragmaArgs KwSearchTimeOut = [ANat]
export
Show KwPragma where
show kw = case kw of
KwHint => "%hint"
KwHide => "%hide"
KwUnhide => "%unhide"
KwLogging => "%logging"
Expand All @@ -126,7 +129,8 @@ Show KwPragma where
export
allPragmas : List KwPragma
allPragmas =
[ KwHide
[ KwHint
, KwHide
, KwUnhide
, KwLogging
, KwAutoLazy
Expand Down

0 comments on commit d99a48b

Please sign in to comment.