ca30292 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #979 from david-christiansen/feature/apropos

:apropos improvements

commitca3029275f3926b9bc5cfe4ebdc5735e6e0a0227 authorEdwin Brady <edwin.brady@gmail.com> dateThu 20 Mar 2014, 11:38 (13 years ago) parent24bfcd8 8c7bde9

4 files changed+24−11

compare with master

unifiedsplit

src/Idris/Apropos.hs+7−4 src/Idris/Docstrings.hs+6−5 src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+9−2

src/Idris/Apropos.hs+7−4

@@ -23,18 +23,21 @@ apropos ist what = let defs = ctxtAlist (tt_ctxt ist)

2323 in nub (map fst (filter (isApropos what) defs) ++

2424 map fst (filter (isApropos what) docs))

2525

26+textIn :: T.Text -> T.Text -> Bool

27+textIn a b = T.isInfixOf (T.toLower a) (T.toLower b)

28+

2629class Apropos a where

2730 isApropos :: T.Text -> a -> Bool

2831

2932instance Apropos Name where

30− isApropos str (UN n) = T.isInfixOf str n

31− isApropos str (NS n' ns) = isApropos str n' || any (T.isInfixOf str) ns

33+ isApropos str (UN n) = textIn str n

34+ isApropos str (NS n' ns) = isApropos str n' || any (textIn str) ns

3235 -- Handle special names from stdlib

3336 isApropos str n | (n == unitTy || n == unitCon) && str == T.pack "()" = True

3437 | n == falseTy && str == T.pack "_|_" = True

3538 | (n == pairTy || n == pairCon) && str == T.pack "," = True

3639 | n == eqTy && str == T.pack "=" = True

37− | n == eqCon && str == T.pack "refl" = True

40+ | n == eqCon && (T.toLower str) == T.pack "refl" = True

3841 | (n == sigmaTy || n == existsCon) && str == T.pack "**" = True

3942 isApropos _ _ = False -- we don't care about case blocks, MNs, etc

4043

@@ -62,7 +65,7 @@ instance Apropos (TT Name) where

6265 isApropos str _ = False

6366

6467instance Apropos Const where

65− isApropos str c = T.isInfixOf str (T.pack (show c))

68+ isApropos str c = textIn str (T.pack (show c))

6669

6770instance Apropos Docstring where

6871 isApropos str d = containsText str d

src/Idris/Docstrings.hs+6−5

@@ -93,25 +93,26 @@ noDocs = (emptyDocstring, [])

9393

9494-- | Does a string occur in the docstring?

9595containsText :: T.Text -> Docstring -> Bool

96−containsText str (CT.Doc _ blocks) = F.any (blockContains str) blocks

96+containsText str (CT.Doc _ blocks) = F.any (blockContains (T.toLower str)) blocks

97+ -- blockContains and inlineContains should always be called with a lower-case search string

9798 where blockContains :: T.Text -> CT.Block -> Bool

9899 blockContains str (CT.Para inlines) = F.any (inlineContains str) inlines

99100 blockContains str (CT.Header lvl inlines) = F.any (inlineContains str) inlines

100101 blockContains str (CT.Blockquote blocks) = F.any (blockContains str) blocks

101102 blockContains str (CT.List b ty blockss) = F.any (F.any (blockContains str)) blockss

102− blockContains str (CT.CodeBlock attr src) = T.isInfixOf str src

103+ blockContains str (CT.CodeBlock attr src) = T.isInfixOf str (T.toLower src)

103104 blockContains str (CT.HtmlBlock txt) = False -- TODO

104105 blockContains str CT.HRule = False

105106

106107 inlineContains :: T.Text -> CT.Inline -> Bool

107− inlineContains str (CT.Str s) = T.isInfixOf str s

108+ inlineContains str (CT.Str s) = T.isInfixOf str (T.toLower s)

108109 inlineContains str CT.Space = False

109110 inlineContains str CT.SoftBreak = False

110111 inlineContains str CT.LineBreak = False

111112 inlineContains str (CT.Emph txt) = F.any (inlineContains str) txt

112113 inlineContains str (CT.Strong txt) = F.any (inlineContains str) txt

113− inlineContains str (CT.Code txt) = T.isInfixOf str txt

114+ inlineContains str (CT.Code txt) = T.isInfixOf str (T.toLower txt)

114115 inlineContains str (CT.Link body url title) = F.any (inlineContains str) body

115116 inlineContains str (CT.Image body url title) = False

116117 inlineContains str (CT.Entity a) = False

117− inlineContains str (CT.RawHtml txt) = T.isInfixOf str txt

118+ inlineContains str (CT.RawHtml txt) = T.isInfixOf str (T.toLower txt)

src/Idris/IdeSlave.hs+2

@@ -135,6 +135,7 @@ data IdeSlaveCommand = REPLCompletions String

135135 | ProofSearch Int String [String]

136136 | LoadFile String

137137 | DocsFor String

138+ | Apropos String

138139 deriving Show

139140

140141sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -153,6 +154,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

153154 StringAtom s -> Just s

154155 _ -> Nothing)

155156sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

157+sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

156158sexpToCommand _ = Nothing

157159

158160parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+9−2

@@ -266,6 +266,8 @@ ideslave orig mods

266266 process stdout fn (MakeWith False line (sUN name))

267267 Just (IdeSlave.ProofSearch line name hints) ->

268268 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

269+ Just (IdeSlave.Apropos a) ->

270+ process stdout fn (Apropos a)

269271 Nothing -> do iPrintError "did not understand")

270272 (\e -> do iPrintError $ show e))

271273 (\e -> do iPrintError $ show e)

@@ -337,6 +339,8 @@ ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False

337339ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)

338340ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

339341 iPrintResult ""

342+ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

343+ iPrintResult ""

340344ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

341345

342346

@@ -962,11 +966,14 @@ process h fn (Apropos a) =

962966 let aproposInfo = [ (n,

963967 delabTy ist n,

964968 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

965− | n <- names ]

969+ | n <- sort names, isUN n ]

966970 ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

967971 where renderApropos impl (name, ty, docs) =

968− prettyName impl [] name <+> colon <+> align (prettyImp impl ty) <$>

972+ prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>

969973 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

974+ isUN (UN _) = True

975+ isUN (NS n _) = isUN n

976+ isUN _ = False

970977

971978classInfo :: ClassInfo -> Idris ()

972979classInfo ci = do iputStrLn "Methods:\n"