45ca5b5 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+4−4

@@ -698,10 +698,10 @@ highlightSource fc annot =

698--

699-- 4. The where block (PDecl' t)

700

701−data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

701+data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

702− | PWith FC Name t [t] t (Maybe Name) [PDecl' t]

702+ | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]

703− | PClauseR FC [t] t [PDecl' t]

703+ | PClauseR FC [t] t [PDecl' t]

704− | PWithR FC [t] t (Maybe Name) [PDecl' t]

704+ | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]

705 deriving Functor

706{-!

707deriving instance Binary PClause'

src/Idris/Elab/Clause.hs+4−1

@@ -837,7 +837,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

837

838 let mpn = case pn_in of

839 Nothing -> Nothing

840− Just n -> Just (uniqueName n (map fst bargs))

840+ Just (n, nfc) -> Just (uniqueName n (map fst bargs))

841+

842+ -- Highlight explicit proofs

843+ sendHighlighting $ [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

841

844

842 logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++

845 logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++

843 " depends on " ++ show pdeps ++ " from " ++ show pvars)

846 " depends on " ++ show pdeps ++ " from " ++ show pvars)

src/Idris/Parser.hs+1−1

@@ -1007,7 +1007,7 @@ clause syn

1007 <?> "function clause"

1008 where

1009 optProof = option Nothing (do reserved "proof"

1010− n <- fst <$> fnName

1010+ n <- fnName

1011 return (Just n))

1012

1013 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause