@@ -402,7 +402,7 @@ simpleExpr syn =
402402 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
403403 <|> proofExpr syn
404404 <|> tacticsExpr syn
405− <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
405+ <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
406406 <|> do reserved "AnyType"; return $ PUniverse AllTypes
407407 <|> PType <$> reservedFC "Type"
408408 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
@@ -462,14 +462,19 @@ bracketed' open syn =
462462 do (FC f start (l, c)) <- getFC
463463 lchar ')'
464464 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
465− <|> try (do (ln, lnfc) <- name
466− colonFC <- lcharFC ':'
467− lty <- expr syn
468− starsFC <- reservedOpFC "**"
465+ <|> try (do (ln, lnfc, colonFC, lty, starsFC):bnds <- some $ do
466+ (ln, lnfc, colonFC) <- try $ do
467+ (ln, lnfc) <- name
468+ colonFC <- lcharFC ':'
469+ return (ln, lnfc, colonFC)
470+ lty <- expr' syn
471+ starsFC <- reservedOpFC "**"
472+ return (ln, lnfc, colonFC, lty, starsFC)
469473 fc <- getFC
470474 r <- expr syn
471475 close <- lcharFC ')'
472− return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))
476+ return (PDPair fc ([open, colonFC, starsFC, close] ++ (=<<) (\(_,_,cfc,_,sfc) -> [cfc, sfc]) bnds)
477+ TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)))
473478 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
474479 -- No prefix operators! (bit of a hack here...)
475480 if (o == "-" || o == "!")
@@ -480,7 +485,7 @@ bracketed' open syn =
480485 <|> try (do l <- simpleExpr syn
481486 op <- option Nothing (do o <- operator
482487 lchar ')'
483− return (Just o))
488+ return (Just o))
484489 fc0 <- getFC
485490 case op of
486491 Nothing -> bracketedExpr syn open l
@@ -489,25 +494,35 @@ bracketed' open syn =
489494 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
490495 <|> do l <- expr syn
491496 bracketedExpr syn open l
492−
497+ where mergePDPairs :: FC -> [(Name, FC, FC, PTerm, FC)] -> PTerm -> PTerm
498+ mergePDPairs starsFC' [] r = r
499+ mergePDPairs starsFC' ((ln, lnfc, colonFC, lty, starsFC):bnds) r =
500+ PDPair starsFC' [] TypeOrTerm (PRef lnfc [] ln) lty (mergePDPairs starsFC bnds r)
501+
493502-- | Parse the contents of parentheses, after an expression has been parsed.
494503bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
495504bracketedExpr syn openParenFC e =
496505 do lchar ')'; return e
497− <|> do exprs <- many (do comma <- lcharFC ','
506+ <|> do exprs <- some (do comma <- lcharFC ','
498507 r <- expr syn
499508 return (r, comma))
500509 closeParenFC <- lcharFC ')'
501510 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
502511 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
503− <|> do starsFC <- reservedOpFC "**"
504− r <- expr syn
512+ <|> do exprs <- some $ do
513+ starsFC <- reservedOpFC "**"
514+ r <- expr syn
515+ return (r, starsFC)
505516 closeParenFC <- lcharFC ')'
506− return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)
517+ let hilite = [openParenFC, closeParenFC] ++ map snd exprs
518+ return (PDPair openParenFC hilite TypeOrTerm e Placeholder (mergePDPairs exprs))
507519 <?> "end of bracketed expression"
508520 where mergePairs :: [(PTerm, FC)] -> PTerm
509521 mergePairs [(t, fc)] = t
510522 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)
523+ mergePDPairs :: [(PTerm, FC)] -> PTerm
524+ mergePDPairs [(t, fc)] = t
525+ mergePDPairs ((t, fc):rs) = PDPair fc [] TypeOrTerm t Placeholder (mergePDPairs rs)
511526
512527-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
513528-- big integer, otherwise try fromInteger and the constants as alternatives.