7ce4d90 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -1207,6 +1207,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1207 colour UnderlineText = IdrisColour Nothing True True False False

1208 colour ItalicText = IdrisColour Nothing True False False True

1209consoleDecorate ist (AnnTerm _ _) = id

1210+consoleDecorate ist (AnnSearchResult _) = id

1210

1211

1211isPostulateName :: Name -> IState -> Bool

1212isPostulateName :: Name -> IState -> Bool

1212isPostulateName n ist = S.member n (idris_postulates ist)

1213isPostulateName n ist = S.member n (idris_postulates ist)

src/Idris/Core/TT.hs+1

@@ -102,6 +102,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

102 | AnnFC FC

103 | AnnTextFmt TextFormatting

104 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term

105+ | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific

105

106

106-- | Used for error reflection

107-- | Used for error reflection

107data ErrorReportPart = TextPart String

108data ErrorReportPart = TextPart String

src/Idris/IdeSlave.hs+6

@@ -145,6 +145,12 @@ instance SExpable OutputAnnotation where

145 ItalicText -> "italic"

146 UnderlineText -> "underline"

147 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]

148+ toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

149+ StringAtom ("Result type is " ++ descr))]

150+ where descr = case ordr of

151+ EQ -> "isomorphic"

152+ LT -> "more general than searched type"

153+ GT -> "more specific than searched type"

148

154

149encodeTerm :: [(Name, Bool)] -> Term -> String

155encodeTerm :: [(Name, Bool)] -> Term -> String

150encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

156encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

src/Idris/TypeSearch.hs+8−7

@@ -34,7 +34,7 @@ import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

34

35import Prelude hiding (pred)

36

37−import Util.Pretty (text, char, vsep, (<>), Doc)

37+import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

38

39searchByType :: PTerm -> Idris ()

40searchByType pterm = do

@@ -173,13 +173,14 @@ data Score = Score

173 , asymMods :: !(Sided AsymMods)

174 } deriving (Eq, Show)

175

176−displayScore :: Score -> Doc a

176+displayScore :: Score -> Doc OutputAnnotation

177−displayScore score = text $ case both noMods (asymMods score) of

177+displayScore score = case both noMods (asymMods score) of

178− Sided True True -> "=" -- types are isomorphic

178+ Sided True True -> annotated EQ "=" -- types are isomorphic

179− Sided True False -> "<" -- found type is more general than searched type

179+ Sided True False -> annotated LT "<" -- found type is more general than searched type

180− Sided False True -> ">" -- searched type is more general than found type

180+ Sided False True -> annotated GT ">" -- searched type is more general than found type

181− Sided False False -> "_"

181+ Sided False False -> text "_"

182 where

183+ annotated ordr = annotate (AnnSearchResult ordr) . text

183 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0

184 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0

184

185

185scoreCriterion :: Score -> Bool

186scoreCriterion :: Score -> Bool