49fffbc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1982 from david-christiansen/feature/ide-doc-overview

49fffbcDavid Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+3−1

compare with master

unifiedsplit

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

336deriving instance NFData Codegen

337!-}

338

339+data HowMuchDocs = FullDocs | OverviewDocs

340+

339-- | REPL commands

341-- | REPL commands

340data Command = Quit

342data Command = Quit

341 | Help

343 | Help

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

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

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

344 | Undefine [Name]

346 | Undefine [Name]

345 | Check PTerm

347 | Check PTerm

346− | DocStr (Either Name Const)

348+ | DocStr (Either Name Const) HowMuchDocs

347 | TotCheck Name

349 | TotCheck Name

348 | Reload

350 | Reload

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

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

src/Idris/Docs.hs+40−28

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

1−{-# LANGUAGE PatternGuards #-}

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

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

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

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6import Idris.Delaborate

7import Idris.Core.TT

8import 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)

11import Util.Pretty

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

18--

19-- Issue #1573 on the Issue tracker.

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

21−data FunDoc = FD Name (Docstring DocTerm)

21+data FunDoc' d = FD Name d

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

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

23− PTerm -- function type

23+ PTerm -- function type

24− (Maybe Fixity)

24+ (Maybe Fixity)

25−

25+ deriving Functor

26+

27+type FunDoc = FunDoc' (Docstring DocTerm)

28+

26−data Docs = FunDoc FunDoc

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

27− | DataDoc FunDoc -- type constructor docs

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

28− [FunDoc] -- data constructor docs

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

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

32+ | ClassDoc Name d -- class docs

30− [FunDoc] -- method docs

33+ [FunDoc' d] -- method docs

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

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

32− [PTerm] -- instances

35+ [PTerm] -- instances

33− [PTerm] -- superclasses

36+ [PTerm] -- superclasses

34− | ModDoc [String] -- Module name

37+ | ModDoc [String] -- Module name

38+ d

39+ deriving Functor

40+

35− (Docstring DocTerm)

41+type Docs = Docs' (Docstring DocTerm)

37showDoc ist d

43showDoc ist d

38 | nullDocstring d = empty

44 | nullDocstring d = empty

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

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

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

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

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

146

152

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

154+-- wants to see

155+howMuch FullDocs = id

156+howMuch OverviewDocs = overview

157+

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

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

148-- documentation object for it

159-- documentation object for it

149−getDocs :: Name -> Idris Docs

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

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

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

151 = do i <- getIState

162 = do i <- getIState

152 case lookupCtxtExact n (idris_moduledocs i) of

163 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

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

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

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

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

156−getDocs n

167+getDocs n w

157 = do i <- getIState

168 = do i <- getIState

158− case lookupCtxt n (idris_classes i) of

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

159− [ci] -> docClass n ci

170+ [ci] -> docClass n ci

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

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

161− [ti] -> docData n ti

172+ [ti] -> docData n ti

162− _ -> do fd <- docFun n

173+ _ -> do fd <- docFun n

163− return (FunDoc fd)

174+ return (FunDoc fd)

175+ return $ fmap (howMuch w) docs

164

176

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

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

166docData n ti

178docData n ti

src/Idris/IdeMode.hs+8−3

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

3{-# 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

7import Text.Printf

8import Numeric

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

206

207data Opt = ShowImpl | ErrContext deriving Show

208

209+data WhatDocs = Overview | Full

210+

209data IdeModeCommand = REPLCompletions String

211data IdeModeCommand = REPLCompletions String

210 | Interpret String

212 | Interpret String

211 | TypeOf String

213 | TypeOf String

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

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

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

218 | MakeLemma Int String

220 | MakeLemma Int String

219 | LoadFile String (Maybe Int)

221 | LoadFile String (Maybe Int)

220− | DocsFor String

222+ | DocsFor String WhatDocs

221 | Apropos String

223 | Apropos String

222 | GetOpts

224 | GetOpts

223 | SetOpt Opt Bool

225 | SetOpt Opt Bool

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

258 _ -> Nothing)

260 _ -> Nothing)

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

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

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

262sexpToCommand (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)]

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

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

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

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

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

269sexpToCommand (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

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

274 -> IO (Maybe Docs)

275loadDocs ist n

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

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

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

278 Left _ -> return Nothing

279 | otherwise = return Nothing

src/Idris/Prover.hs+2−2

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

202 receiveInput h e

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

204 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))

206 _ -> return Nothing

207

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

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

336 return (False, e, False, prf,

337 Right $ iRenderResult (vsep toShow)))

338 (\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

340 return $ pprintDocs ist doc

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

342 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) =

344 Left err -> iPrintError err

345 Right n -> process "(idemode)"

346 (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) =

348 case parseConst orig name of

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

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

350 Failure _ ->

351 case splitName name of

352 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

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

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

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

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

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

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

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

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

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

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

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

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

557idemodeProcess 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)

557idemodeProcess fn Universes = process fn Universes

559idemodeProcess fn Universes = process fn Universes

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

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

559 iPrintResult ""

561 iPrintResult ""

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

905 _ -> iPrintTermWithType (pprintDelab ist tm)

907 _ -> iPrintTermWithType (pprintDelab ist tm)

906 (pprintDelab ist ty)

908 (pprintDelab ist ty)

907

909

908−process fn (DocStr (Left n))

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

909 = do ist <- getIState

911 = do ist <- getIState

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

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

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

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

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

912 case docs of

915 case docs of

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

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

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

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

915 iRenderResult (vsep toShow)

918 iRenderResult (vsep toShow)

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

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

917 return $ pprintDocs ist doc

920 return $ pprintDocs ist doc

921+

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

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

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

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

920 modDocN _ = sMN 1 "NotFoundForSure"

924 modDocN _ = sMN 1 "NotFoundForSure"

921

925

922−process fn (DocStr (Right c))

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

923 = do ist <- getIState

927 = do ist <- getIState

924 iRenderResult $ pprintConstDocs ist c (constDocs c)

928 iRenderResult $ pprintConstDocs ist c (constDocs c)

925

929

src/Idris/REPLParser.hs+2−2

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

258 let constant = do

259 c <- P.constant

260 eof

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

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

262

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

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

264

265 try constant <|> fnName

266