c6f1061 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove vestiges of pre-SpecialName names

commitc6f1061a7feb50bbe6373af5c3e51166aad251e7 authorMelvar Chen <Melvar.Chen@googlemail.com> dateTue 31 May 2016, 22:18 (10 years ago) parent22792d2

3 files changed+2−8

unifiedsplit

src/Idris/Completion.hs−2

@@ -39,8 +39,6 @@ tactics = map fst tacticArgs

3939-- | Convert a name into a string usable for completion. Filters out names

4040-- that users probably don't want to see.

4141nameString :: Name -> Maybe String

42−nameString (UN nm)

43− | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing

4442nameString (UN n) = Just (str n)

4543nameString (NS n _) = nameString n

4644nameString _ = Nothing

src/Idris/Core/TT.hs+1−2

@@ -598,8 +598,7 @@ mapCtxt = fmap . fmap

598598

599599-- |Return True if the argument 'Name' should be interpreted as the name of a

600600-- typeclass.

601−tcname (UN xs) | T.null xs = False

602− | otherwise = T.head xs == '@'

601+tcname (UN xs) = False

603602tcname (NS n _) = tcname n

604603tcname (SN (InstanceN _ _)) = True

605604tcname (SN (MethodN _)) = True

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

@@ -791,12 +791,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

791791 mkLHSapp t = t

792792

793793 decorate (NS x ns)

794− = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])

795−-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

794+ = NS (SN (WhereN cnum fname x)) ns

796795 decorate x

797796 = SN (WhereN cnum fname x)

798−-- = NS (SN (WhereN cnum fname x)) [show cnum]

799−-- = NS (UN ('#':show x)) [show cnum, show fname]

800797

801798 sepBlocks bs = sepBlocks' [] bs where

802799 sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)