83793a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add the ability for IDEs to get documentation overviews

This adds an optional second argument to the documentation command in the IDE protocol. If it is the symbol :overview, then only the overview part of the docstring is returned. This is intended for use in things like completion engines or Emacs's eldoc.

commit83793a6631aa83d7bd47c2814c2944381179bc1e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 6 Mar 2015, 16:26 (12 years ago) parentec13063

7 files changed+68−45

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Docs.hs+40−28 src/Idris/IdeMode.hs+8−3 src/Idris/IdrisDoc.hs+1−1 src/Idris/Prover.hs+2−2 src/Idris/REPL.hs+12−8 src/Idris/REPLParser.hs+2−2

src/Idris/AbsSyntaxTree.hs+3−1

@@ -336,6 +336,8 @@ data Codegen = Via String

336336deriving instance NFData Codegen

337337!-}

338338

339+data HowMuchDocs = FullDocs | OverviewDocs

340+

339341-- | REPL commands

340342data Command = Quit

341343 | Help

@@ -343,7 +345,7 @@ data Command = Quit

343345 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

344346 | Undefine [Name]

345347 | Check PTerm

346− | DocStr (Either Name Const)

348+ | DocStr (Either Name Const) HowMuchDocs

347349 | TotCheck Name

348350 | Reload

349351 | Load FilePath (Maybe Int) -- up to maximum line number

src/Idris/Docs.hs+40−28

@@ -1,12 +1,12 @@

1−{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where

1+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

2+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

66import Idris.Delaborate

77import Idris.Core.TT

88import Idris.Core.Evaluate

9−import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm)

9+import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)

1010

1111import Util.Pretty

1212

@@ -18,21 +18,27 @@ import qualified Data.Text as T

1818--

1919-- Issue #1573 on the Issue tracker.

2020-- https://github.com/idris-lang/Idris-dev/issues/1573

21−data FunDoc = FD Name (Docstring DocTerm)

22− [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] -- args: name, ty, implicit, docs

23− PTerm -- function type

24− (Maybe Fixity)

25−

26−data Docs = FunDoc FunDoc

27− | DataDoc FunDoc -- type constructor docs

28− [FunDoc] -- data constructor docs

29− | ClassDoc Name (Docstring DocTerm)-- class docs

30− [FunDoc] -- method docs

31− [(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings

32− [PTerm] -- instances

33− [PTerm] -- superclasses

34− | ModDoc [String] -- Module name

35− (Docstring DocTerm)

21+data FunDoc' d = FD Name d

22+ [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs

23+ PTerm -- function type

24+ (Maybe Fixity)

25+ deriving Functor

26+

27+type FunDoc = FunDoc' (Docstring DocTerm)

28+

29+data Docs' d = FunDoc (FunDoc' d)

30+ | DataDoc (FunDoc' d) -- type constructor docs

31+ [FunDoc' d] -- data constructor docs

32+ | ClassDoc Name d -- class docs

33+ [FunDoc' d] -- method docs

34+ [(Name, Maybe d)] -- parameters and their docstrings

35+ [PTerm] -- instances

36+ [PTerm] -- superclasses

37+ | ModDoc [String] -- Module name

38+ d

39+ deriving Functor

40+

41+type Docs = Docs' (Docstring DocTerm)

3642

3743showDoc ist d

3844 | nullDocstring d = empty

@@ -144,23 +150,29 @@ pprintDocs ist (ModDoc mod docs)

144150 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

145151 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

146152

153+-- | Determine a truncation function depending how much docs the user

154+-- wants to see

155+howMuch FullDocs = id

156+howMuch OverviewDocs = overview

157+

147158-- | Given a fully-qualified, disambiguated name, construct the

148159-- documentation object for it

149−getDocs :: Name -> Idris Docs

150−getDocs n@(NS n' ns) | n' == modDocName

160+getDocs :: Name -> HowMuchDocs -> Idris Docs

161+getDocs n@(NS n' ns) w | n' == modDocName

151162 = do i <- getIState

152163 case lookupCtxtExact n (idris_moduledocs i) of

153− Just doc -> return $ ModDoc (reverse (map T.unpack ns)) doc

164+ Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc

154165 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++

155166 " do not exist! This shouldn't have happened and is a bug."

156−getDocs n

167+getDocs n w

157168 = do i <- getIState

158− case lookupCtxt n (idris_classes i) of

159− [ci] -> docClass n ci

160− _ -> case lookupCtxt n (idris_datatypes i) of

161− [ti] -> docData n ti

162− _ -> do fd <- docFun n

163− return (FunDoc fd)

169+ docs <- case lookupCtxt n (idris_classes i) of

170+ [ci] -> docClass n ci

171+ _ -> case lookupCtxt n (idris_datatypes i) of

172+ [ti] -> docData n ti

173+ _ -> do fd <- docFun n

174+ return (FunDoc fd)

175+ return $ fmap (howMuch w) docs

164176

165177docData :: Name -> TypeInfo -> Idris Docs

166178docData n ti

src/Idris/IdeMode.hs+8−3

@@ -2,7 +2,7 @@

33{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

5−module Idris.IdeMode(parseMessage, convSExp, IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

5+module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

77import Text.Printf

88import Numeric

@@ -206,6 +206,8 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

206206

207207data Opt = ShowImpl | ErrContext deriving Show

208208

209+data WhatDocs = Overview | Full

210+

209211data IdeModeCommand = REPLCompletions String

210212 | Interpret String

211213 | TypeOf String

@@ -217,7 +219,7 @@ data IdeModeCommand = REPLCompletions String

217219 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

218220 | MakeLemma Int String

219221 | LoadFile String (Maybe Int)

220− | DocsFor String

222+ | DocsFor String WhatDocs

221223 | Apropos String

222224 | GetOpts

223225 | SetOpt Opt Bool

@@ -258,7 +260,10 @@ sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAt

258260 _ -> Nothing)

259261sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

260262sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

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

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

264+sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])

265+ | Just w <- lookup s opts = Just (DocsFor name w)

266+ where opts = [("overview", Overview), ("full", Full)]

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

263268sexpToCommand (SymbolAtom "get-options") = Just GetOpts

264269sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

src/Idris/IdrisDoc.hs+1−1

@@ -273,7 +273,7 @@ loadDocs :: IState -- ^ IState to extract infomation from

273273 -> Name -- ^ Name to load Docs for

274274 -> IO (Maybe Docs)

275275loadDocs ist n

276− | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n) ist

276+ | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n FullDocs) ist

277277 case docs of Right d -> return (Just d)

278278 Left _ -> return Nothing

279279 | otherwise = return Nothing

src/Idris/Prover.hs+2−2

@@ -202,7 +202,7 @@ receiveInput h e =

202202 receiveInput h e

203203 Just (IdeMode.Interpret cmd) -> return (Just cmd)

204204 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))

205− Just (IdeMode.DocsFor str) -> return (Just (":doc " ++ str))

205+ Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))

206206 _ -> return Nothing

207207

208208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

@@ -336,7 +336,7 @@ ploop fn d prompt prf e h

336336 return (False, e, False, prf,

337337 Right $ iRenderResult (vsep toShow)))

338338 (\err -> do putIState ist ; ierror err)

339− where showDoc ist (n, d) = do doc <- getDocs n

339+ where showDoc ist (n, d) = do doc <- getDocs n FullDocs

340340 return $ pprintDocs ist doc

341341 docStr (Right c) = do ist <- getIState

342342 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

src/Idris/REPL.hs+12−8

@@ -344,13 +344,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

344344 Left err -> iPrintError err

345345 Right n -> process "(idemode)"

346346 (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

347−runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =

347+runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

348348 case parseConst orig name of

349− Success c -> process "(idemode)" (DocStr (Right c))

349+ Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

350350 Failure _ ->

351351 case splitName name of

352352 Left err -> iPrintError err

353− Right n -> process "(idemode)" (DocStr (Left n))

353+ Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

354+ where howMuch IdeMode.Overview = OverviewDocs

355+ howMuch IdeMode.Full = FullDocs

354356runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355357 process fn (CaseSplitAt False line (sUN name))

356358runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

@@ -553,7 +555,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)

553555idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

554556idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

555557idemodeProcess fn (Check t) = process fn (Check t)

556−idemodeProcess fn (DocStr n) = process fn (DocStr n)

558+idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

557559idemodeProcess fn Universes = process fn Universes

558560idemodeProcess fn (Defn n) = do process fn (Defn n)

559561 iPrintResult ""

@@ -905,21 +907,23 @@ process fn (Check t)

905907 _ -> iPrintTermWithType (pprintDelab ist tm)

906908 (pprintDelab ist ty)

907909

908−process fn (DocStr (Left n))

910+process fn (DocStr (Left n) w)

909911 = do ist <- getIState

910912 let docs = lookupCtxtName n (idris_docstrings ist) ++

911− map (\(n,d)-> (n, (d,[]))) (lookupCtxtName (modDocN n) (idris_moduledocs ist))

913+ map (\(n,d)-> (n, (d, [])))

914+ (lookupCtxtName (modDocN n) (idris_moduledocs ist))

912915 case docs of

913916 [] -> iPrintError $ "No documentation for " ++ show n

914917 ns -> do toShow <- mapM (showDoc ist) ns

915918 iRenderResult (vsep toShow)

916− where showDoc ist (n, d) = do doc <- getDocs n

919+ where showDoc ist (n, d) = do doc <- getDocs n w

917920 return $ pprintDocs ist doc

921+

918922 modDocN (NS (UN n) ns) = NS modDocName (n:ns)

919923 modDocN (UN n) = NS modDocName [n]

920924 modDocN _ = sMN 1 "NotFoundForSure"

921925

922−process fn (DocStr (Right c))

926+process fn (DocStr (Right c) _) -- constants only have overviews

923927 = do ist <- getIState

924928 iRenderResult $ pprintConstDocs ist c (constDocs c)

925929

src/Idris/REPLParser.hs+2−2

@@ -258,9 +258,9 @@ cmd_doc name = do

258258 let constant = do

259259 c <- P.constant

260260 eof

261− return $ Right (DocStr (Right c))

261+ return $ Right (DocStr (Right c) FullDocs)

262262

263− let fnName = fnNameArg (\n -> DocStr (Left n)) name

263+ let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

264264

265265 try constant <|> fnName

266266