9071856 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make isTConName and friends exact

They should only be used in a disambiguated context anyway to avoid it picking the wrong one. Before this change, the coloring was wrong on :let data A = A.A :t A Now it is fixed.

commit907185639d6d3a33d81add8a501c756df4083dc1 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 2 Feb 2015, 00:41 (12 years ago) parenta87f69e

2 files changed+22−26

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+21−25 src/Idris/Delaborate.hs+1−1

src/Idris/Core/Evaluate.hs+21−25

@@ -971,47 +971,43 @@ isConName n ctxt = isTConName n ctxt || isDConName n ctxt

971971

972972isTConName :: Name -> Context -> Bool

973973isTConName n ctxt

974− = or $ do def <- lookupCtxt n (definitions ctxt)

975− case tfst def of

976− (TyDecl (TCon _ _) _) -> return True

977− _ -> return False

974+ = case lookupDefExact n ctxt of

975+ Just (TyDecl (TCon _ _) _) -> True

976+ _ -> False

978977

979978isDConName :: Name -> Context -> Bool

980979isDConName n ctxt

981− = or $ do def <- lookupCtxt n (definitions ctxt)

982− case tfst def of

983− (TyDecl (DCon _ _ _) _) -> return True

984− _ -> return False

980+ = case lookupDefExact n ctxt of

981+ Just (TyDecl (DCon _ _ _) _) -> True

982+ _ -> False

985983

986984isFnName :: Name -> Context -> Bool

987985isFnName n ctxt

988− = let def = lookupCtxtExact n (definitions ctxt) in

989− case def of

990− Just (Function _ _, _, _, _) -> True

991− Just (Operator _ _ _, _, _, _) -> True

992− Just (CaseOp _ _ _ _ _ _, _, _, _) -> True

993− _ -> False

986+ = case lookupDefExact n ctxt of

987+ Just (Function _ _) -> True

988+ Just (Operator _ _ _) -> True

989+ Just (CaseOp _ _ _ _ _ _) -> True

990+ _ -> False

994991

995992isTCDict :: Name -> Context -> Bool

996993isTCDict n ctxt

997− = let def = lookupCtxtExact n (definitions ctxt) in

998− case def of

999− Just (Function _ _, _, _, _) -> False

1000− Just (Operator _ _ _, _, _, _) -> False

1001− Just (CaseOp ci _ _ _ _ _, _, _, _) -> tc_dictionary ci

1002− _ -> False

994+ = case lookupDefExact n ctxt of

995+ Just (Function _ _) -> False

996+ Just (Operator _ _ _) -> False

997+ Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

998+ _ -> False

1003999

10041000lookupP :: Name -> Context -> [Term]

10051001lookupP n ctxt

10061002 = do def <- lookupCtxt n (definitions ctxt)

10071003 p <- case def of

1008− (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1009− (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1004+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1005+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

10101006 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1011− (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1007+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

10121008 case snd p of

1013− Hidden -> []

1014− _ -> return (fst p)

1009+ Hidden -> []

1010+ _ -> return (fst p)

10151011

10161012lookupDefExact :: Name -> Context -> Maybe Def

10171013lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

src/Idris/Delaborate.hs+1−1

@@ -488,7 +488,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

488488 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

489489 _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

490490 _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

491− _ | otherwise -> annot

491+ _ | otherwise -> annot

492492 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

493493 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

494494 let o = overview (fst docs)