@@ -1054,15 +1054,15 @@ RHS ::= '=' Expr
1054RHSName ::= '{' FnName '}';
1054RHSName ::= '{' FnName '}';
1057−rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
1057+rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
1058rhs syn n = do lchar '='
1058rhs syn n = do lchar '='
1059 indentGt
1059 indentGt
1060− expr syn
1060+ withExtent $ expr syn
1061 <|> do symbol "?=";
1061 <|> do symbol "?=";
1062 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1062 (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")
1063 r <- expr syn
1063 r <- expr syn
1064− return (addLet fc name r)
1064+ return (addLet fc name r, fc)
1065− <|> impossible
1065+ <|> withExtent impossible
1066 <?> "function right hand side"
1066 <?> "function right hand side"
1067 where mkN :: Name -> Name
1067 where mkN :: Name -> Name
1068 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
1068 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
@@ -1104,33 +1104,34 @@ WhereOrTerminator ::= WhereBlock | Terminator;
1104clause :: SyntaxInfo -> IdrisParser PClause
1104clause :: SyntaxInfo -> IdrisParser PClause
1105clause syn
1105clause syn
1106 -- unnamed with or function clause (inside a with)
1106 -- unnamed with or function clause (inside a with)
1108− wargs <- P.try (do pushIndent; some (wExpr syn))
1107+ = do wargs <- P.try (do pushIndent; some (wExpr syn))
1109 ist <- get
1108 ist <- get
1110 n <- case lastParse ist of
1109 n <- case lastParse ist of
1111 Just t -> return t
1110 Just t -> return t
1112 Nothing -> fail "Invalid clause"
1111 Nothing -> fail "Invalid clause"
1113− (do r <- rhs syn n
1112+ (do (r, fc) <- rhs syn n
1114 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1113 let wsyn = syn { syn_namespace = [], syn_toplevel = False }
1115 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1114 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1116 <|> ([], []) <$ terminator
1115 <|> ([], []) <$ terminator
1117− return $ \fc -> PClauseR fc wargs r wheres) <|> (do
1116+ return $ PClauseR fc wargs r wheres) <|> (do
1118 popIndent
1117 popIndent
1118+ ((wval, pn), fc) <- withExtent $ do
1119− keyword "with"
1119+ keyword "with"
1120− wval <- simpleExpr syn
1120+ wval <- bracketed syn
1121− pn <- optProof
1121+ pn <- optProof
1122 openBlock
1123 openBlock
1123 ds <- some $ fnDecl syn
1124 ds <- some $ fnDecl syn
1124 let withs = concat ds
1125 let withs = concat ds
1125 closeBlock
1126 closeBlock
1126− return $ \fc -> PWithR fc wargs wval pn withs))
1127+ return $ PWithR fc wargs wval pn withs)
1128 <|> do ty <- P.try (do pushIndent
1129 <|> do ty <- P.try (do pushIndent
1129 ty <- simpleExpr syn
1130 ty <- simpleExpr syn
1130 symbol "<=="
1131 symbol "<=="
1131 return ty)
1132 return ty)
1132 (n, fc) <- withExtent (expandNS syn <$> fnName)
1133 (n, fc) <- withExtent (expandNS syn <$> fnName)
1133− r <- rhs syn n
1134+ (r, _) <- rhs syn n
1134 let wsyn = syn { syn_namespace = [] }
1135 let wsyn = syn { syn_namespace = [] }
1135 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1136 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1136 <|> ([], []) <$ terminator
1137 <|> ([], []) <$ terminator
@@ -1145,7 +1146,7 @@ clause syn
1145 <|> do pushIndent
1146 <|> do pushIndent
1146 (n, nfc, capp, wargs) <- lhs
1147 (n, nfc, capp, wargs) <- lhs
1147 modify $ \ist -> ist { lastParse = Just n }
1148 modify $ \ist -> ist { lastParse = Just n }
1148− (do (rs, fc) <- withExtent (rhs syn n)
1149+ (do (rs, fc) <- rhs syn n
1149 let wsyn = syn { syn_namespace = [] }
1150 let wsyn = syn { syn_namespace = [] }
1150 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1151 (wheres, nmap) <- whereBlock n wsyn <* popIndent
1151 <|> ([], []) <$ terminator
1152 <|> ([], []) <$ terminator