[ fix ] preserve spacing during update

src/Idris/IDEMode/CaseSplit.idr

@@ -56,22 +56,23 @@ doUpdates : {auto u : Ref UPD (List String)} ->
             Core (List SourcePart)
 doUpdates defs ups [] = pure []
 doUpdates defs ups (LBrace :: xs)
-    = case dropSpace xs of
+    = let (ws, nws) = spanSpace xs in map (LBrace :: ws ++) $
+         case nws of
            Name n :: RBrace :: rest =>
-                pure (LBrace :: Name n ::
+                pure (Name n ::
                       Whitespace " " :: Equal :: Whitespace " " ::
                       !(doUpdates defs ups (Name n :: RBrace :: rest)))
            Name n :: Equal :: rest =>
-                pure (LBrace :: Name n ::
+                pure (Name n ::
                       Whitespace " " :: Equal :: Whitespace " " ::
                       !(doUpdates defs ups rest))
-           _ => pure (LBrace :: !(doUpdates defs ups xs))
+           _ => doUpdates defs ups xs
   where
-    dropSpace : List SourcePart -> List SourcePart
+    spanSpace : List SourcePart -> (List SourcePart, List SourcePart)
-    dropSpace [] = []
+    spanSpace []                   = ([], [])
-    dropSpace (RBrace :: xs) = RBrace :: xs
+    spanSpace (RBrace           :: xs) = ([], RBrace :: xs)
-    dropSpace (Whitespace _ :: xs) = dropSpace xs
+    spanSpace (w@(Whitespace _) :: xs) = mapFst (w ::) (spanSpace xs)
-    dropSpace (x :: xs) = x :: dropSpace xs
+    spanSpace (x                :: xs) = map    (x ::) (spanSpace xs)
 doUpdates defs ups (Name n :: xs)
     = case lookup n ups of
            Nothing => pure (Name n :: !(doUpdates defs ups xs))

tests/Main.idr

@@ -52,6 +52,7 @@ idrisTests
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
+       "interactive013",
        -- Literate
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",

tests/idris2/interactive013/Spacing.idr

@@ -0,0 +1,4 @@
+module Spacing
+
+id : {n : Nat} -> Nat
+id {  n} = ?a

tests/idris2/interactive013/expected

@@ -0,0 +1,5 @@
+1/1: Building Spacing (Spacing.idr)
+Spacing> id {  n = 0} = ?a_1
+id {  n = (S k)} = ?a_2
+Spacing> 
+Bye for now!

tests/idris2/interactive013/input

@@ -0,0 +1,2 @@
+:cs 4 6 n
+:q

tests/idris2/interactive013/run

@@ -0,0 +1,3 @@
+$1 --no-banner Spacing.idr < input
+
+rm -rf build