Add compatibility with the original record update syntax.

docs/source/reference/records.rst

@@ -178,8 +178,12 @@ Finally, the examples:
       -- prints 3.0
       printLn $ (record { topLeft.x = 3 } rect).topLeft.x
 
+      -- but for compatibility, we support the old syntax, too
+      printLn $ (record { topLeft->x = 3 } rect).topLeft.x
+
       -- prints 2.1
       printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
+      printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
 
 Parses but does not typecheck:
 

src/Idris/Parser.idr

@@ -651,7 +651,7 @@ mutual
 
   field : FileName -> IndentInfo -> Rule PFieldUpdate
   field fname indents
-      = do path <- map fieldName <$> [| name :: many recField |]
+      = do path <- map fieldName <$> [| name :: many recFieldCompat |]
            upd <- (do symbol "="; pure PSetField)
                       <|>
                   (do symbol "$="; pure PSetFieldApp)
@@ -663,6 +663,11 @@ mutual
       fieldName (RF s) = s
       fieldName _ = "_impossible"
 
+      -- this allows the dotted syntax .field
+      -- but also the arrowed syntax ->field for compatibility with Idris 1
+      recFieldCompat : Rule Name
+      recFieldCompat = recField <|> (symbol "->" *> name)
+
   rewrite_ : FileName -> IndentInfo -> Rule PTerm
   rewrite_ fname indents
       = do start <- location

tests/idris2/record004/expected

@@ -23,4 +23,6 @@ Main> 4.2
 Main> 4.2
 Main> 3
 Main> 2.1
+Main> 3
+Main> 2.1
 Main> Bye for now!

tests/idris2/record004/input

@@ -18,4 +18,6 @@ Point.x pt
 x pt
 (record { topLeft.x = 3 } rect).topLeft.x
 (record { topLeft.x $= (+1) } rect).topLeft.x
+(record { topLeft->x = 3 } rect).topLeft.x
+(record { topLeft->x $= (+1) } rect).topLeft.x
 :q