[ refactor ] get rid of ad-hoc function getLine

idris2.ipkg

@@ -52,6 +52,7 @@ modules =
     Data.Bool.Extra,
     Data.IntMap,
     Data.LengthMatch,
+    Data.List.Extra,
     Data.NameMap,
     Data.StringMap,
     Data.These,

src/Data/List/Extra.idr

@@ -0,0 +1,11 @@
+module Data.List.Extra
+
+%default covering
+
+||| Fetches the element at a given position.
+||| Returns `Nothing` if the position beyond the list's end.
+public export
+elemAt : List a -> Nat -> Maybe a
+elemAt []        _     = Nothing
+elemAt (l :: _)  Z     = Just l
+elemAt (_ :: ls) (S n) = elemAt ls n

src/Idris/IDEMode/CaseSplit.idr

@@ -19,16 +19,12 @@ import Idris.Resugar
 import Idris.Syntax
 
 import Data.List
+import Data.List.Extra
 import Data.Strings
 import System.File
 
 %default covering
 
-getLine : Nat -> List String -> Maybe String
-getLine Z (l :: ls) = Just l
-getLine (S k) (l :: ls) = getLine k ls
-getLine _ [] = Nothing
-
 toStrUpdate : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               (Name, RawImp) -> Core (List (String, String))
@@ -135,7 +131,7 @@ updateCase splits line col
               Just f =>
                 do Right file <- coreLift $ readFile f
                        | Left err => throw (FileErr f err)
-                   let thisline = getLine (integerToNat (cast line)) (lines file)
+                   let thisline = elemAt (lines file) (integerToNat (cast line))
                    case thisline of
                         Nothing => throw (InternalError "File too short!")
                         Just l =>