[ fix #1741 ] Do not replace names in as-patterns

src/Idris/IDEMode/CaseSplit.idr

@@ -110,6 +110,9 @@ doUpdates defs ups (LBrace :: xs)
                              )
           -- not a special case: proceed as normal
           _ => pure (LBrace :: [] ++ !(doUpdates defs ups xs))
+-- if we have a name that acts as an as-pattern then do not update it
+doUpdates defs ups (Name n :: AsPattern :: xs)
+    = pure $ Name n :: AsPattern :: !(doUpdates defs ups xs)
 -- if we have a name, look up if it's a name we're updating. If it isn't, keep
 -- the old name, otherwise update the name, i.e. replace with the new name
 doUpdates defs ups (Name n :: xs)

src/Idris/IDEMode/TokenLine.idr

@@ -18,6 +18,7 @@ data SourcePart
   | LBrace
   | RBrace
   | Equal
+  | AsPattern
   | Other String
 
 ------------------------------------------------------------------------
@@ -32,6 +33,7 @@ toString (HoleName n) = "?" ++ n
 toString LBrace = "{"
 toString RBrace = "}"
 toString Equal = "="
+toString AsPattern = "@"
 toString (Other str) = str
 
 ------------------------------------------------------------------------
@@ -49,6 +51,7 @@ srcTokens =
      (is '{', const LBrace),
      (is '}', const RBrace),
      (is '=', const Equal),
+     (is '@', const AsPattern),
      (any, Other)]
 
 export

tests/Main.idr

@@ -88,7 +88,8 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
        "interactive025", "interactive026", "interactive027", "interactive028",
        "interactive029", "interactive030", "interactive031", "interactive032",
        "interactive033", "interactive034", "interactive035", "interactive036",
-       "interactive037", "interactive038", "interactive039", "interactive040"]
+       "interactive037", "interactive038", "interactive039", "interactive040",
+       "interactive041"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool "Interface" [] Nothing

tests/idris2/interactive041/Issue1741.idr

@@ -0,0 +1,4 @@
+import Data.Fin
+
+foo : (n : Nat) -> (i : Fin n) -> Bool
+foo n@(_) i = ?foo_rhs

tests/idris2/interactive041/expected

@@ -0,0 +1,5 @@
+1/1: Building Issue1741 (Issue1741.idr)
+Main> foo n@(_) FZ = ?foo_rhs_0
+foo n@(_) (FS x) = ?foo_rhs_1
+Main> 
+Bye for now!

tests/idris2/interactive041/input

@@ -0,0 +1,2 @@
+:cs 4 10 i
+:q

tests/idris2/interactive041/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner Issue1741.idr < input