@@ -1054,15 +1054,15 @@ RHS ::= '=' Expr
10541054RHSName ::= '{' FnName '}';
10551055@
10561056-}
1057−rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1057+rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
10581058rhs syn n = do lchar '='
10591059 indentGt
1060− expr syn
1060+ withExtent $ expr syn
10611061 <|> do symbol "?=";
10621062 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
10631063 r <- expr syn
1064− return (addLet fc name r)
1065− <|> impossible
1064+ return (addLet fc name r, fc)
1065+ <|> withExtent impossible
10661066 <?> "function right hand side"
10671067 where mkN :: Name -> Name
10681068 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
@@ -1104,33 +1104,34 @@ WhereOrTerminator ::= WhereBlock | Terminator;
11041104clause :: SyntaxInfo -> IdrisParser PClause
11051105clause syn
11061106 -- unnamed with or function clause (inside a with)
1107− = appExtent (do
1108− wargs <- P.try (do pushIndent; some (wExpr syn))
1107+ = do wargs <- P.try (do pushIndent; some (wExpr syn))
11091108 ist <- get
11101109 n <- case lastParse ist of
11111110 Just t -> return t
11121111 Nothing -> fail "Invalid clause"
1113− (do r <- rhs syn n
1112+ (do (r, fc) <- rhs syn n
11141113 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
11151114 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11161115 <|> ([], []) <$ terminator
1117− return $ \fc -> PClauseR fc wargs r wheres) <|> (do
1116+ return $ PClauseR fc wargs r wheres) <|> (do
11181117 popIndent
1119− keyword "with"
1120− wval <- simpleExpr syn
1121− pn <- optProof
1118+ ((wval, pn), fc) <- withExtent $ do
1119+ keyword "with"
1120+ wval <- bracketed syn
1121+ pn <- optProof
1122+ return (wval, pn)
11221123 openBlock
11231124 ds <- some $ fnDecl syn
11241125 let withs = concat ds
11251126 closeBlock
1126− return $ \fc -> PWithR fc wargs wval pn withs))
1127+ return $ PWithR fc wargs wval pn withs)
11271128 -- <==
11281129 <|> do ty <- P.try (do pushIndent
11291130 ty <- simpleExpr syn
11301131 symbol "<=="
11311132 return ty)
11321133 (n, fc) <- withExtent (expandNS syn <$> fnName)
1133− r <- rhs syn n
1134+ (r, _) <- rhs syn n
11341135 let wsyn = syn { syn_namespace = [] }
11351136 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11361137 <|> ([], []) <$ terminator
@@ -1145,7 +1146,7 @@ clause syn
11451146 <|> do pushIndent
11461147 (n, nfc, capp, wargs) <- lhs
11471148 modify $ \ist -> ist { lastParse = Just n }
1148− (do (rs, fc) <- withExtent (rhs syn n)
1149+ (do (rs, fc) <- rhs syn n
11491150 let wsyn = syn { syn_namespace = [] }
11501151 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11511152 <|> ([], []) <$ terminator