mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-03 00:55:00 +03:00
[ fuzzysearch ] don't print holes
This commit is contained in:
parent
7bd7f1da9c
commit
a6a4593aba
@ -53,7 +53,7 @@ fuzzySearch expr = do
|
||||
guard (isJust $ userNameRoot (fullname d))
|
||||
pure d
|
||||
allDefs <- traverse (resolved ctxt) defs
|
||||
filterM (\def => fuzzyMatch neg pos def.type) allDefs
|
||||
filterM (predicate neg pos) allDefs
|
||||
put Ctxt defs
|
||||
doc <- traverse (docsOrSignature EmptyFC) $ fullname <$> filteredDefs
|
||||
pure $ PrintedDoc $ vsep doc
|
||||
@ -153,3 +153,11 @@ fuzzySearch expr = do
|
||||
let refsB = doFind [] tm
|
||||
refsB <- traverse toFullNames' refsB
|
||||
pure (isNil $ diffBy isApproximationOf' pos refsB)
|
||||
|
||||
predicate : (neg : List NameOrConst)
|
||||
-> (pos : List NameOrConst)
|
||||
-> GlobalDef
|
||||
-> Core Bool
|
||||
predicate neg pos def = case definition def of
|
||||
Hole{} => pure False
|
||||
_ => fuzzyMatch neg pos def.type
|
||||
|
Loading…
Reference in New Issue
Block a user