@@ -337,45 +337,49 @@ bracketed syn =
337337 do lchar ')'
338338 fc <- getFC
339339 return $ PTrue fc
340− <|>
341− try (do l <- expr syn
342− lchar ')'
343− return l)
344− <|> do (l, fc) <- try (do
345− l <- expr syn
346− fc <- getFC
347− lchar ','
348− return (l, fc))
349− rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
350− lchar ')'
351− return $ PPair fc l (mergePairs rs)
352− <|> do (l, fc) <- try (do
353− l <- expr syn
354− fc <- getFC
355− reservedOp "**"
356− return (l, fc))
357− r <- expr syn
358− lchar ')'
359− return (PDPair fc l Placeholder r)
360− <|> try(do fc0 <- getFC
361− l <- expr' syn
362− o <- operator
363− lchar ')'
364− return $ PLam (sMN 1000 "ARG") Placeholder
365− (PApp fc0 (PRef fc0 (sUN o)) [pexp l,
366− pexp (PRef fc0 (sMN 1000 "ARG"))]))
367− <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
368− return $ PLam (sMN 1000 "ARG") Placeholder
369− (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),
370− pexp e]))
371− <|> try (do ln <- name; lchar ':'
340+ <|> try (do ln <- name; lchar ':';
372341 lty <- expr syn
373342 reservedOp "**"
374343 fc <- getFC
375344 r <- expr syn
376345 lchar ')'
377346 return (PDPair fc (PRef fc ln) lty r))
378− <?> "end of braced expression"
347+ <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
348+ -- No prefix operators! (bit of a hack here...)
349+ if (o == "-" || o == "!")
350+ then fail "minus not allowed in section"
351+ else return $ PLam (sMN 1000 "ARG") Placeholder
352+ (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),
353+ pexp e]))
354+ <|> try (do l <- simpleExpr syn
355+ op <- option Nothing (do o <- operator
356+ lchar ')'
357+ return (Just o))
358+ fc0 <- getFC
359+ case op of
360+ Nothing -> bracketedExpr syn l
361+ Just o -> return $ PLam (sMN 1000 "ARG") Placeholder
362+ (PApp fc0 (PRef fc0 (sUN o)) [pexp l,
363+ pexp (PRef fc0 (sMN 1000 "ARG"))]))
364+ <|> do l <- expr syn
365+ bracketedExpr syn l
366+
367+bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm
368+bracketedExpr syn e =
369+ do lchar ')'; return e
370+ <|> do fc <- do fc <- getFC
371+ lchar ','
372+ return fc
373+ rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
374+ lchar ')'
375+ return $ PPair fc e (mergePairs rs)
376+ <|> do fc <- do fc <- getFC
377+ reservedOp "**"
378+ return fc
379+ r <- expr syn
380+ lchar ')'
381+ return (PDPair fc e Placeholder r)
382+ <?> "end of bracketed expression"
379383 where mergePairs :: [(PTerm, FC)] -> PTerm
380384 mergePairs [(t, fc)] = t
381385 mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)