fix: help menu for refine command (idris-lang#3393)

* remove reference to column number parameter * update contributors and changelog_next * fix expected test output
andrevidela · Dec 17, 2024 · d70242d · d70242d
1 parent ab51b18
commit d70242d
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 5 deletions.
diff --git 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
@@ -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
@@ -2241,7 +2241,7 @@ knownCommands =
   explain ["mc", "makecase"] "Make case on term <n> defined on line <l>" ++
   explain ["mw", "makewith"] "Add with expression on term <n> defined on line <l>" ++
   [ ("intro", "Introduce unambiguous constructor in hole <n> defined on line <l>")
-  , ("refine", "Refine hole <h> with identifier <n> on line <l> and column <c>")
+  , ("refine", "Refine hole <h> with identifier <n> on line <l>")
   ] ++
   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
@@ -34,7 +34,7 @@ Main>  <expr>                                                Evaluate an express
  :mc :makecase     <l:number> <n:string>               Make case on term <n> defined on line <l>
  :mw :makewith     <l:number> <n:string>               Add with expression on term <n> defined on line <l>
  :intro            <l:number> <n:string>               Introduce unambiguous constructor in hole <n> defined on line <l>
- :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :refine           <l:number> <h:string> <e:expr>      Refine hole <h> with identifier <n> on line <l>
  :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
  :psnext                                               Show next proof
  :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search
@@ -79,7 +79,7 @@ Main>  <expr>                                                Evaluate an express
  :mc :makecase     <l:number> <n:string>               Make case on term <n> defined on line <l>
  :mw :makewith     <l:number> <n:string>               Add with expression on term <n> defined on line <l>
  :intro            <l:number> <n:string>               Introduce unambiguous constructor in hole <n> defined on line <l>
- :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :refine           <l:number> <h:string> <e:expr>      Refine hole <h> with identifier <n> on line <l>
  :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
  :psnext                                               Show next proof
  :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search
@@ -124,7 +124,7 @@ Main>  <expr>                                                Evaluate an express
  :mc :makecase     <l:number> <n:string>               Make case on term <n> defined on line <l>
  :mw :makewith     <l:number> <n:string>               Add with expression on term <n> defined on line <l>
  :intro            <l:number> <n:string>               Introduce unambiguous constructor in hole <n> defined on line <l>
- :refine           <l:number> <c:number> <h:string> <e:expr>Refine hole <h> with identifier <n> on line <l> and column <c>
+ :refine           <l:number> <h:string> <e:expr>      Refine hole <h> with identifier <n> on line <l>
  :ps :proofsearch  <l:number> <n:string> <h:[name]>    Search for a proof
  :psnext                                               Show next proof
  :gd               <l:number> <n:string> <r:number|0>  Try to generate a definition using proof-search