From 263d9e8ad0cf312735d68aa7150630b7a50b55c1 Mon Sep 17 00:00:00 2001 From: Justin Date: Sun, 24 Nov 2024 16:59:30 -0500 Subject: [PATCH] fix: help menu for `refine` command (#3393) * remove reference to column number parameter * update contributors and changelog_next * fix expected test output --- CHANGELOG_NEXT.md | 2 ++ CONTRIBUTORS | 1 + src/Idris/Parser.idr | 3 +-- tests/idris2/repl/repl001/expected | 6 +++--- 4 files changed, 7 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 9b6d965bf2..2e5c753c35 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -25,6 +25,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO where Idris2 will install the given package if `idris2 --install {ipkg-filename}` is called. +* Remove reference to column number parameter in help menu for `refine` command. + ### Building/Packaging changes * The Nix flake's `buildIdris` function now returns a set with `executable` and diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 5e36d08394..d0b2f997d7 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -40,6 +40,7 @@ Jens Petersen Joel Berkeley Joey Eremondi Johann Rudloff +Justin Yang Kamil Shakirov Kevin Boulain LuoChen diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 2ac708c2e1..66ee8d17c7 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -2241,7 +2241,7 @@ knownCommands = explain ["mc", "makecase"] "Make case on term defined on line " ++ explain ["mw", "makewith"] "Add with expression on term defined on line " ++ [ ("intro", "Introduce unambiguous constructor in hole defined on line ") - , ("refine", "Refine hole with identifier on line and column ") + , ("refine", "Refine hole with identifier on line ") ] ++ explain ["ps", "proofsearch"] "Search for a proof" ++ [ ("psnext", "Show next proof") @@ -2587,7 +2587,6 @@ editLineNamePTermArgCmd : ParseCmd -> (Bool -> Int -> Name -> PTerm -> EditCmd) editLineNamePTermArgCmd parseCmd command doc = ( names , Args [ NamedCmdArg "l" NumberArg - , NamedCmdArg "c" NumberArg , NamedCmdArg "h" StringArg , NamedCmdArg "e" ExprArg ] diff --git a/tests/idris2/repl/repl001/expected b/tests/idris2/repl/repl001/expected index 97b5a6afb4..36add07727 100644 --- a/tests/idris2/repl/repl001/expected +++ b/tests/idris2/repl/repl001/expected @@ -34,7 +34,7 @@ Main> Evaluate an express :mc :makecase Make case on term defined on line :mw :makewith Add with expression on term defined on line :intro Introduce unambiguous constructor in hole defined on line - :refine Refine hole with identifier on line and column + :refine Refine hole with identifier on line :ps :proofsearch Search for a proof :psnext Show next proof :gd Try to generate a definition using proof-search @@ -79,7 +79,7 @@ Main> Evaluate an express :mc :makecase Make case on term defined on line :mw :makewith Add with expression on term defined on line :intro Introduce unambiguous constructor in hole defined on line - :refine Refine hole with identifier on line and column + :refine Refine hole with identifier on line :ps :proofsearch Search for a proof :psnext Show next proof :gd Try to generate a definition using proof-search @@ -124,7 +124,7 @@ Main> Evaluate an express :mc :makecase Make case on term defined on line :mw :makewith Add with expression on term defined on line :intro Introduce unambiguous constructor in hole defined on line - :refine Refine hole with identifier on line and column + :refine Refine hole with identifier on line :ps :proofsearch Search for a proof :psnext Show next proof :gd Try to generate a definition using proof-search