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

git.iko.soy/Idris-dev

Accurate highlighting of proof bindings on the with rule

commit45ca5b58e5a30ac80614af926e3bb9e9fec66bd7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 11 May 2015, 16:50 (11 years ago) parent0419a12

3 files changed+9−6

compare with master

unifiedsplit

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

src/Idris/AbsSyntaxTree.hs+4−4

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

698698--

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

700700

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]

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

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

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, FC)) [PDecl' t]

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

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

705705 deriving Functor

706706{-!

707707deriving 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)

837837

838838 let mpn = case pn_in of

839839 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]

841844

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

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

src/Idris/Parser.hs+1−1

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

10071007 <?> "function clause"

10081008 where

10091009 optProof = option Nothing (do reserved "proof"

1010− n <- fst <$> fnName

1010+ n <- fnName

10111011 return (Just n))

10121012

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