git.iko.soy/Idris-dev
on master help sign in
Save terms in docstrings

Now, when elaborating definitions, terms included in `code blocks` in docstrings are elaborated in the context that results from the definition that they document. This means that they get semantic coloring at the REPL, and IDEs can provide features like showing implicits and further definition chasing.

commit37292e185685cb1539ae76fa232783f0c9909567 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 30 Sep 2014, 15:33 (12 years ago) parent4694a36
24 files changed+443−250
compare with master
unifiedsplit
CHANGELOG+1 libs/prelude/Prelude/Bool.idr+1−1 src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+16−20 src/Idris/Apropos.hs+1−1 src/Idris/DeepSeq.hs+31−31 src/Idris/Delaborate.hs+2−1 src/Idris/Docs.hs+18−14 src/Idris/Docstrings.hs+199−74 src/Idris/Elab/Class.hs+2−2 src/Idris/Elab/Data.hs+16−9 src/Idris/Elab/Provider.hs+1−1 src/Idris/Elab/Record.hs+2−2 src/Idris/Elab/Type.hs+15−6 src/Idris/Elab/Utils.hs+2−2 src/Idris/Elab/Value.hs+11−1 src/Idris/IBC.hs+48−47 src/Idris/IdrisDoc.hs+7−7 src/Idris/Output.hs+10 src/Idris/ParseData.hs+27−13 src/Idris/ParseExpr.hs+6 src/Idris/ParseHelpers.hs+2−2 src/Idris/Parser.hs+22−13 src/Idris/TypeSearch.hs+2−2
CHANGELOG+1
@@ -21,6 +21,7 @@ New in 0.9.15:
2121* New REPL command :printdef displays the internal definition of a name
2222* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting
2323* Naming of data and type constructors is made consistent across the standard library (see #1516)
24+* Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs.
2425
2526New in 0.9.14:
2627--------------
libs/prelude/Prelude/Bool.idr+1−1
@@ -21,7 +21,7 @@ boolElim False t e = e
2121||| if you need to perform a Boolean test and convince the type checker of this
2222||| fact.
2323|||
24−||| If you find yourself using `so` for something other than primitive types,
24+||| If you find yourself using `So` for something other than primitive types,
2525||| it may be appropriate to define a type of evidence for the property that you
2626||| care about instead.
2727data So : Bool -> Type where
src/Idris/AbsSyntax.hs+1−1
@@ -279,7 +279,7 @@ addCoercion :: Name -> Idris ()
279279addCoercion n = do i <- getIState
280280 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
281281
282−addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
282+addDocStr :: Name -> Docstring (Maybe Term) -> [(Name, Docstring (Maybe Term))] -> Idris ()
283283addDocStr n doc args
284284 = do i <- getIState
285285 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
src/Idris/AbsSyntaxTree.hs+16−20
@@ -158,7 +158,7 @@ data IState = IState {
158158 idris_flags :: Ctxt [FnOpt],
159159 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
160160 idris_calledgraph :: Ctxt [Name],
161− idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
161+ idris_docstrings :: Ctxt (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]),
162162 idris_tyinfodata :: Ctxt TIData,
163163 idris_fninfo :: Ctxt FnInfo,
164164 idris_totcheck :: [(FC, Name)], -- names to check totality on
@@ -535,19 +535,19 @@ type ProvideWhat = ProvideWhat' PTerm
535535-- datatypes and typeclasses.
536536data PDecl' t
537537 = PFix FC Fixity [String] -- ^ Fixity declaration
538− | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
539− | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
538+ | PTy (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
539+ | PPostulate (Docstring (Maybe PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
540540 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
541541 | PCAF FC Name t -- ^ Top level constant
542− | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
542+ | PData (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
543543 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
544544 | PNamespace String [PDecl' t] -- ^ New namespace
545− | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
546− | PClass Docstring SyntaxInfo FC
545+ | PRecord (Docstring (Maybe PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Maybe PTerm)) Name t -- ^ Record declaration
546+ | PClass (Docstring (Maybe PTerm)) SyntaxInfo FC
547547 [t] -- constraints
548548 Name
549549 [(Name, t)] -- parameters
550− [(Name, Docstring)] -- parameter docstrings
550+ [(Name, Docstring (Maybe PTerm))] -- parameter docstrings
551551 [PDecl' t] -- declarations
552552 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
553553 -- class name, parameters, method declarations
@@ -598,7 +598,7 @@ deriving instance NFData PClause'
598598-- | Data declaration
599599data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
600600 d_tcon :: t, -- ^ Type constructor
601− d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
601+ d_cons :: [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, t, FC, [Name])] -- ^ Constructors
602602 }
603603 -- ^ Data declaration
604604 | PLaterdecl { d_name :: Name, d_tcon :: t }
@@ -1071,7 +1071,8 @@ primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
10711071unitTy = sUN "Unit"
10721072unitCon = sUN "MkUnit"
10731073
1074−falseDoc = parseDocstring . T.pack $
1074+-- TODO: elaborate the code samples in the docstring
1075+falseDoc = fmap (const Nothing) . parseDocstring . T.pack $
10751076 "The empty type, also known as the trivially false proposition." ++
10761077 "\n\n" ++
10771078 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
@@ -1085,7 +1086,7 @@ pairCon = sUN "MkPair"
10851086
10861087eqTy = sUN "="
10871088eqCon = sUN "Refl"
1088−eqDoc = parseDocstring . T.pack $
1089+eqDoc = fmap (const Nothing) . parseDocstring . T.pack $
10891090 "The propositional equality type. A proof that `x` = `y`." ++
10901091 "\n\n" ++
10911092 "To use such a proof, pattern-match on it, and the two equal things will " ++
@@ -1108,14 +1109,14 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
11081109 pexp (PRef bi (n "x")),
11091110 pexp (PRef bi (n "x"))])), bi, [])]
11101111 where n a = sUN a
1111− reflDoc = parseDocstring . T.pack $
1112+ reflDoc = annotCode (const Nothing) . parseDocstring . T.pack $
11121113 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
11131114 "shown that both sides are in fact equal."
1114− reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1115− (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1115+ reflParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1116+ (n "x", annotCode (const Nothing) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
11161117
1117−eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1118− (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1118+eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1119+ (n "B", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")
11191120 ]
11201121 where n a = sUN a
11211122
@@ -1464,11 +1465,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
14641465 getFixity :: String -> Maybe Fixity
14651466 getFixity = flip M.lookup fixities
14661467
1467−prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
1468−prettyDocumentedIst ist (name, ty, docs) =
1469− prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1470− fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1471−
14721468-- | Pretty-printer helper for the binding site of a name
14731469bindingOf :: Name -- ^^ the bound name
14741470 -> Bool -- ^^ whether the name is implicit
src/Idris/Apropos.hs+1−1
@@ -71,7 +71,7 @@ instance Apropos (TT Name) where
7171instance Apropos Const where
7272 isApropos str c = textIn str (T.pack (show c))
7373
74−instance Apropos Docstring where
74+instance Apropos (Docstring a) where
7575 isApropos str d = containsText str d
7676
7777instance (Apropos a, Apropos b) => Apropos (a, b) where
src/Idris/DeepSeq.hs+31−31
@@ -7,46 +7,46 @@ import Idris.AbsSyntaxTree
77import Control.DeepSeq
88
99import qualified Cheapskate.Types as CT
10+import qualified Idris.Docstrings as D
1011
11−-- Manual from imported libs
12−instance NFData CT.Doc where
13− rnf (CT.Doc opts contents) = rnf opts `seq` rnf contents `seq` ()
12+instance NFData a => NFData (D.Docstring a) where
13+ rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()
1414
1515instance NFData CT.Options where
16− rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
17−
18−instance NFData CT.Block where
19− rnf (CT.Para lines) = rnf lines `seq` ()
20− rnf (CT.Header i lines) = rnf i `seq` rnf lines `seq` ()
21− rnf (CT.Blockquote bs) = rnf bs `seq` ()
22− rnf (CT.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()
23− rnf (CT.CodeBlock attr txt) = rnf attr `seq` rnf txt `seq` ()
24− rnf (CT.HtmlBlock txt) = rnf txt `seq` ()
25− rnf CT.HRule = ()
26−
27−instance NFData CT.Inline where
28− rnf (CT.Str txt) = rnf txt `seq` ()
29− rnf CT.Space = ()
30− rnf CT.SoftBreak = ()
31− rnf CT.LineBreak = ()
32− rnf (CT.Emph xs) = rnf xs `seq` ()
33− rnf (CT.Strong xs) = rnf xs `seq` ()
34− rnf (CT.Code xs) = rnf xs `seq` ()
35− rnf (CT.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()
36− rnf (CT.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()
37− rnf (CT.Entity a) = rnf a `seq` ()
38− rnf (CT.RawHtml x) = rnf x `seq` ()
16+ rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
17+
18+instance NFData a => NFData (D.Block a) where
19+ rnf (D.Para lines) = rnf lines `seq` ()
20+ rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()
21+ rnf (D.Blockquote bs) = rnf bs `seq` ()
22+ rnf (D.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()
23+ rnf (D.CodeBlock attr txt tm) = rnf attr `seq` rnf txt `seq` ()
24+ rnf (D.HtmlBlock txt) = rnf txt `seq` ()
25+ rnf D.HRule = ()
26+
27+instance NFData a => NFData (D.Inline a) where
28+ rnf (D.Str txt) = rnf txt `seq` ()
29+ rnf D.Space = ()
30+ rnf D.SoftBreak = ()
31+ rnf D.LineBreak = ()
32+ rnf (D.Emph xs) = rnf xs `seq` ()
33+ rnf (D.Strong xs) = rnf xs `seq` ()
34+ rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()
35+ rnf (D.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()
36+ rnf (D.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()
37+ rnf (D.Entity a) = rnf a `seq` ()
38+ rnf (D.RawHtml x) = rnf x `seq` ()
3939
4040instance NFData CT.ListType where
41− rnf (CT.Bullet c) = rnf c `seq` ()
42− rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
41+ rnf (CT.Bullet c) = rnf c `seq` ()
42+ rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
4343
4444instance NFData CT.CodeAttr where
45− rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
45+ rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
4646
4747instance NFData CT.NumWrapper where
48− rnf CT.PeriodFollowing = ()
49− rnf CT.ParenFollowing = ()
48+ rnf CT.PeriodFollowing = ()
49+ rnf CT.ParenFollowing = ()
5050
5151-- All generated by 'derive'
5252
src/Idris/Delaborate.hs+2−1
@@ -428,7 +428,8 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
428428 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
429429 let o = overview (fst docs)
430430 -- TODO make width configurable
431− out = displayS . renderPretty 1.0 50 $ renderDocstring o
431+ out = displayS . renderPretty 1.0 50 $
432+ renderDocstring (pprintDelab ist) o
432433 return (out "")
433434 getTy :: IState -> Name -> String -- fails if name not already extant!
434435 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
src/Idris/Docs.hs+18−14
@@ -6,7 +6,7 @@ import Idris.AbsSyntaxTree
66import Idris.Delaborate
77import Idris.Core.TT
88import Idris.Core.Evaluate
9−import Idris.Docstrings
9+import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring)
1010
1111import Util.Pretty
1212
@@ -16,8 +16,8 @@ import qualified Data.Text as T
1616
1717-- TODO: Only include names with public/abstract accessibility
1818
19−data FunDoc = FD Name Docstring
20− [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs
19+data FunDoc = FD Name (Docstring (Maybe Term))
20+ [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs
2121 PTerm -- function type
2222 (Maybe Fixity)
2323 deriving Show
@@ -25,22 +25,22 @@ data FunDoc = FD Name Docstring
2525data Docs = FunDoc FunDoc
2626 | DataDoc FunDoc -- type constructor docs
2727 [FunDoc] -- data constructor docs
28− | ClassDoc Name Docstring -- class docs
28+ | ClassDoc Name (Docstring (Maybe Term))-- class docs
2929 [FunDoc] -- method docs
30− [(Name, Maybe Docstring)] -- parameters and their docstrings
30+ [(Name, Maybe (Docstring (Maybe Term)))] -- parameters and their docstrings
3131 [PTerm] -- instances
3232 [PTerm] -- superclasses
3333 deriving Show
3434
35−showDoc d | nullDocstring d = empty
36− | otherwise = text " -- " <> renderDocstring d
35+showDoc ist d | nullDocstring d = empty
36+ | otherwise = text " -- " <> renderDocstring (pprintDelab ist) d
3737
3838pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
3939pprintFD ist (FD n doc args ty f)
4040 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
4141 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
4242 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
43− renderDocstring doc <$>
43+ renderDocstring (pprintDelab ist) doc <$>
4444 maybe empty (\f -> text (show f) <> line) f <>
4545 let argshow = showArgs args [] in
4646 if not (null argshow)
@@ -52,19 +52,19 @@ pprintFD ist (FD n doc args ty f)
5252 showArgs ((n, ty, Exp {}, Just d):args) bnd
5353 = bindingOf n False <+> colon <+>
5454 pprintPTerm ppo bnd [] infixes ty <>
55− showDoc d <> line
55+ showDoc ist d <> line
5656 :
5757 showArgs args ((n, False):bnd)
5858 showArgs ((n, ty, Constraint {}, Just d):args) bnd
5959 = text "Class constraint" <+>
60− pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line
60+ pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
6161 :
6262 showArgs args ((n, True):bnd)
6363 showArgs ((n, ty, Imp {}, Just d):args) bnd
6464 = text "(implicit)" <+>
6565 bindingOf n True <+> colon <+>
6666 pprintPTerm ppo bnd [] infixes ty <>
67− showDoc d <> line
67+ showDoc ist d <> line
6868 :
6969 showArgs args ((n, True):bnd)
7070 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
@@ -80,7 +80,9 @@ pprintDocs ist (DataDoc t args)
8080 vsep (map (pprintFD ist) args))
8181pprintDocs ist (ClassDoc n doc meths params instances superclasses)
8282 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
83− if nullDocstring doc then empty else line <> renderDocstring doc)
83+ if nullDocstring doc
84+ then empty
85+ else line <> renderDocstring (pprintDelab ist) doc)
8486 <> line <$>
8587 nest 4 (text "Parameters:" <$> prettyParameters)
8688 <> line <$>
@@ -131,7 +133,7 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)
131133 (subclasses, instances') = partition isSubclass instances
132134
133135 prettyParameters = if any (isJust . snd) params
134− then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty showDoc md) params)
136+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
135137 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
136138
137139getDocs :: Name -> Idris Docs
@@ -185,7 +187,7 @@ docFun n
185187 funName n
186188 | n == falseTy = "_|_"
187189
188−getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
190+getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]
189191getPArgNames (PPi plicity name ty body) ds =
190192 (name, ty, plicity, lookup name ds) : getPArgNames body ds
191193getPArgNames _ _ = []
@@ -201,3 +203,5 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty
201203 t (Str _) = PConstant StrType
202204 t (Ch c) = PConstant $ AType (ATInt ITChar)
203205 t _ = PType
206+
207+
src/Idris/Docstrings.hs+199−74
@@ -1,26 +1,90 @@
1+{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3+
14-- | Wrapper around Markdown library
25module Idris.Docstrings (
3− Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,
4− overview, containsText
6+ Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,
7+ overview, containsText, renderHtml, annotCode
58 ) where
69
710import qualified Cheapskate as C
811import qualified Cheapskate.Types as CT
12+import Cheapskate.Html (renderDoc)
913
1014import Util.Pretty
1115
12−import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name)
16+import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term)
1317
1418import qualified Data.Text as T
1519import qualified Data.Foldable as F
20+import Data.Foldable (Foldable)
21+import Data.Traversable (Traversable)
1622import qualified Data.Sequence as S
1723
18−-- | Representation of Idris's inline documentation
19−type Docstring = CT.Doc
24+import Control.DeepSeq (NFData(..))
25+
26+import Text.Blaze.Html (Html)
27+
28+-- | Representation of Idris's inline documentation. The type paramter
29+-- represents the type of terms that are associated with code blocks.
30+data Docstring a = DocString CT.Options (Blocks a)
31+ deriving (Show, Functor, Foldable, Traversable)
32+
33+type Blocks a = S.Seq (Block a)
34+
35+-- | Block-level elements.
36+data Block a = Para (Inlines a)
37+ | Header Int (Inlines a)
38+ | Blockquote (Blocks a)
39+ | List Bool CT.ListType [Blocks a]
40+ | CodeBlock CT.CodeAttr T.Text a
41+ | HtmlBlock T.Text
42+ | HRule
43+ deriving (Show, Functor, Foldable, Traversable)
44+
45+data Inline a = Str T.Text
46+ | Space
47+ | SoftBreak
48+ | LineBreak
49+ | Emph (Inlines a)
50+ | Strong (Inlines a)
51+ | Code T.Text a
52+ | Link (Inlines a) T.Text T.Text
53+ | Image (Inlines a) T.Text T.Text
54+ | Entity T.Text
55+ | RawHtml T.Text
56+ deriving (Show, Functor, Foldable, Traversable)
57+
58+type Inlines a = S.Seq (Inline a)
59+
2060
2161-- | Construct a docstring from a Text that contains Markdown-formatted docs
22−parseDocstring :: T.Text -> CT.Doc
23−parseDocstring = C.markdown options
62+parseDocstring :: T.Text -> Docstring ()
63+parseDocstring = toDocstring . C.markdown options
64+ where toDocstring :: CT.Doc -> Docstring ()
65+ toDocstring (CT.Doc opts blocks) = DocString opts (fmap toBlock blocks)
66+
67+ toBlock :: CT.Block -> Block ()
68+ toBlock (CT.Para inlines) = Para (fmap toInline inlines)
69+ toBlock (CT.Header i inlines) = Header i (fmap toInline inlines)
70+ toBlock (CT.Blockquote blocks) = Blockquote (fmap toBlock blocks)
71+ toBlock (CT.List b t blocks) = List b t (fmap (fmap toBlock) blocks)
72+ toBlock (CT.CodeBlock attrs text) = CodeBlock attrs text ()
73+ toBlock (CT.HtmlBlock src) = HtmlBlock src
74+ toBlock CT.HRule = HRule
75+
76+ toInline :: CT.Inline -> Inline ()
77+ toInline (CT.Str t) = Str t
78+ toInline CT.Space = Space
79+ toInline CT.SoftBreak = SoftBreak
80+ toInline CT.LineBreak = LineBreak
81+ toInline (CT.Emph is) = Emph (fmap toInline is)
82+ toInline (CT.Strong is) = Strong (fmap toInline is)
83+ toInline (CT.Code src) = Code src ()
84+ toInline (CT.Link is url title) = Link (fmap toInline is) url title
85+ toInline (CT.Image is url title) = Image (fmap toInline is) url title
86+ toInline (CT.Entity txt) = Entity txt
87+ toInline (CT.RawHtml src) = RawHtml src
2488
2589
2690options = CT.Options { CT.sanitize = True
@@ -30,90 +94,151 @@ options = CT.Options { CT.sanitize = True
3094 }
3195
3296-- | Convert a docstring to be shown by the pretty-printer
33−renderDocstring :: Docstring -> Doc OutputAnnotation
34−renderDocstring (CT.Doc _ blocks) = renderBlocks blocks
97+renderDocstring :: (a -> Doc OutputAnnotation) -> Docstring (Maybe a) -> Doc OutputAnnotation
98+renderDocstring pp (DocString _ blocks) = renderBlocks pp blocks
3599
36100-- | Construct a docstring consisting of the first block-level element of the
37101-- argument docstring, for use in summaries.
38−overview :: Docstring -> Docstring
39−overview (CT.Doc opts blocks) = CT.Doc opts (S.take 1 blocks)
40−
41−renderBlocks :: CT.Blocks -> Doc OutputAnnotation
42−renderBlocks blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $
43− fmap renderBlock blocks
44− | S.length blocks == 1 = renderBlock (S.index blocks 0)
45− | otherwise = empty
46−
47−renderBlock :: CT.Block -> Doc OutputAnnotation
48−renderBlock (CT.Para inlines) = renderInlines inlines
49−renderBlock (CT.Header lvl inlines) = renderInlines inlines <+> parens (text (show lvl))
50−renderBlock (CT.Blockquote blocks) = indent 8 $ renderBlocks blocks
51−renderBlock (CT.List b ty blockss) = renderList b ty blockss
52−renderBlock (CT.CodeBlock attr src) = indent 8 $ text (T.unpack src)
53−renderBlock (CT.HtmlBlock txt) = text "<html block>" -- TODO
54−renderBlock CT.HRule = text "----------------------"
55−
56−renderList :: Bool -> CT.ListType -> [CT.Blocks] -> Doc OutputAnnotation
57−renderList b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks) blockss
58−renderList b (CT.Numbered nw i) blockss =
102+overview :: Docstring a -> Docstring a
103+overview (DocString opts blocks) = DocString opts (S.take 1 blocks)
104+
105+renderBlocks :: (a -> Doc OutputAnnotation) -> Blocks (Maybe a) -> Doc OutputAnnotation
106+renderBlocks pp blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $
107+ fmap (renderBlock pp) blocks
108+ | S.length blocks == 1 = renderBlock pp (S.index blocks 0)
109+ | otherwise = empty
110+
111+renderBlock :: (a -> Doc OutputAnnotation) -> Block (Maybe a) -> Doc OutputAnnotation
112+renderBlock pp (Para inlines) = renderInlines pp inlines
113+renderBlock pp (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))
114+renderBlock pp (Blockquote blocks) = indent 8 $ renderBlocks pp blocks
115+renderBlock pp (List b ty blockss) = renderList pp b ty blockss
116+renderBlock pp (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)
117+renderBlock pp (CodeBlock attr src (Just tm)) = indent 8 $ pp tm
118+renderBlock pp (HtmlBlock txt) = text "<html block>" -- TODO
119+renderBlock pp HRule = text "----------------------"
120+
121+renderList :: (a -> Doc OutputAnnotation) -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation
122+renderList pp b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp) blockss
123+renderList pp b (CT.Numbered nw i) blockss =
59124 vsep $
60125 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)
61− [i..] (repeat punc) (map renderBlocks blockss)
126+ [i..] (repeat punc) (map (renderBlocks pp) blockss)
62127 where punc = case nw of
63128 CT.PeriodFollowing -> char '.'
64129 CT.ParenFollowing -> char '('
65130
66−renderInlines :: CT.Inlines -> Doc OutputAnnotation
67−renderInlines = F.foldr (<>) empty . fmap renderInline
68−
69−renderInline :: CT.Inline -> Doc OutputAnnotation
70−renderInline (CT.Str s) = text $ T.unpack s
71−renderInline CT.Space = softline
72−renderInline CT.SoftBreak = softline
73−renderInline CT.LineBreak = line
74−renderInline (CT.Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines txt -- TODO
75−renderInline (CT.Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines txt -- TODO
76−renderInline (CT.Code txt) = text $ T.unpack txt
77−renderInline (CT.Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines body) <+>
131+renderInlines :: (a -> Doc OutputAnnotation) -> Inlines (Maybe a) -> Doc OutputAnnotation
132+renderInlines pp = F.foldr (<>) empty . fmap (renderInline pp)
133+
134+renderInline :: (a -> Doc OutputAnnotation) -> Inline (Maybe a) -> Doc OutputAnnotation
135+renderInline pp (Str s) = text $ T.unpack s
136+renderInline pp Space = softline
137+renderInline pp SoftBreak = softline
138+renderInline pp LineBreak = line
139+renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt
140+renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt
141+renderInline pp (Code txt Nothing) = text $ T.unpack txt
142+renderInline pp (Code txt (Just tm)) = pp tm
143+renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>
78144 parens (text $ T.unpack url)
79−renderInline (CT.Image body url title) = text "<image>" -- TODO
80−renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO
81−renderInline (CT.RawHtml txt) = text "<html content>" --TODO
145+renderInline pp (Image body url title) = text "<image>" -- TODO
146+renderInline pp (Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO
147+renderInline pp (RawHtml txt) = text "<html content>" --TODO
82148
83149-- | The empty docstring
84−emptyDocstring :: Docstring
85−emptyDocstring = CT.Doc options S.empty
150+emptyDocstring :: Docstring a
151+emptyDocstring = DocString options S.empty
86152
87153-- | Check whether a docstring is emtpy
88−nullDocstring :: Docstring -> Bool
89−nullDocstring (CT.Doc _ blocks) = S.null blocks
154+nullDocstring :: Docstring a -> Bool
155+nullDocstring (DocString _ blocks) = S.null blocks
90156
91157-- | Empty documentation for a definition
92−noDocs :: (Docstring, [(Name, Docstring)])
158+noDocs :: (Docstring a, [(Name, Docstring a)])
93159noDocs = (emptyDocstring, [])
94160
95161-- | Does a string occur in the docstring?
96−containsText :: T.Text -> Docstring -> Bool
97−containsText str (CT.Doc _ blocks) = F.any (blockContains (T.toLower str)) blocks
162+containsText :: T.Text -> Docstring a -> Bool
163+containsText str (DocString _ blocks) = F.any (blockContains (T.toLower str)) blocks
98164 -- blockContains and inlineContains should always be called with a lower-case search string
99− where blockContains :: T.Text -> CT.Block -> Bool
100− blockContains str (CT.Para inlines) = F.any (inlineContains str) inlines
101− blockContains str (CT.Header lvl inlines) = F.any (inlineContains str) inlines
102− blockContains str (CT.Blockquote blocks) = F.any (blockContains str) blocks
103− blockContains str (CT.List b ty blockss) = F.any (F.any (blockContains str)) blockss
104− blockContains str (CT.CodeBlock attr src) = T.isInfixOf str (T.toLower src)
105− blockContains str (CT.HtmlBlock txt) = False -- TODO
106− blockContains str CT.HRule = False
107−
108− inlineContains :: T.Text -> CT.Inline -> Bool
109− inlineContains str (CT.Str s) = T.isInfixOf str (T.toLower s)
110− inlineContains str CT.Space = False
111− inlineContains str CT.SoftBreak = False
112− inlineContains str CT.LineBreak = False
113− inlineContains str (CT.Emph txt) = F.any (inlineContains str) txt
114− inlineContains str (CT.Strong txt) = F.any (inlineContains str) txt
115− inlineContains str (CT.Code txt) = T.isInfixOf str (T.toLower txt)
116− inlineContains str (CT.Link body url title) = F.any (inlineContains str) body
117− inlineContains str (CT.Image body url title) = False
118− inlineContains str (CT.Entity a) = False
119− inlineContains str (CT.RawHtml txt) = T.isInfixOf str (T.toLower txt)
165+ where blockContains :: T.Text -> Block a -> Bool
166+ blockContains str (Para inlines) = F.any (inlineContains str) inlines
167+ blockContains str (Header lvl inlines) = F.any (inlineContains str) inlines
168+ blockContains str (Blockquote blocks) = F.any (blockContains str) blocks
169+ blockContains str (List b ty blockss) = F.any (F.any (blockContains str)) blockss
170+ blockContains str (CodeBlock attr src _) = T.isInfixOf str (T.toLower src)
171+ blockContains str (HtmlBlock txt) = False -- TODO
172+ blockContains str HRule = False
173+
174+ inlineContains :: T.Text -> Inline a -> Bool
175+ inlineContains str (Str s) = T.isInfixOf str (T.toLower s)
176+ inlineContains str Space = False
177+ inlineContains str SoftBreak = False
178+ inlineContains str LineBreak = False
179+ inlineContains str (Emph txt) = F.any (inlineContains str) txt
180+ inlineContains str (Strong txt) = F.any (inlineContains str) txt
181+ inlineContains str (Code txt _) = T.isInfixOf str (T.toLower txt)
182+ inlineContains str (Link body url title) = F.any (inlineContains str) body
183+ inlineContains str (Image body url title) = False
184+ inlineContains str (Entity a) = False
185+ inlineContains str (RawHtml txt) = T.isInfixOf str (T.toLower txt)
186+
187+
188+renderHtml :: Docstring (Maybe Term) -> Html
189+renderHtml = renderDoc . fromDocstring
190+ where
191+ fromDocstring :: Docstring (Maybe Term) -> CT.Doc
192+ fromDocstring (DocString opts blocks) = CT.Doc opts (fmap fromBlock blocks)
193+
194+ fromBlock :: Block (Maybe Term) -> CT.Block
195+ fromBlock (Para inlines) = CT.Para (fmap fromInline inlines)
196+ fromBlock (Header i inlines) = CT.Header i (fmap fromInline inlines)
197+ fromBlock (Blockquote blocks) = CT.Blockquote (fmap fromBlock blocks)
198+ fromBlock (List b t blocks) = CT.List b t (fmap (fmap fromBlock) blocks)
199+ fromBlock (CodeBlock attrs text _) = CT.CodeBlock attrs text
200+ fromBlock (HtmlBlock src) = CT.HtmlBlock src
201+ fromBlock HRule = CT.HRule
202+
203+ fromInline :: Inline (Maybe Term) -> CT.Inline
204+ fromInline (Str t) = CT.Str t
205+ fromInline Space = CT.Space
206+ fromInline SoftBreak = CT.SoftBreak
207+ fromInline LineBreak = CT.LineBreak
208+ fromInline (Emph is) = CT.Emph (fmap fromInline is)
209+ fromInline (Strong is) = CT.Strong (fmap fromInline is)
210+ fromInline (Code src _) = CT.Code src
211+ fromInline (Link is url title) = CT.Link (fmap fromInline is) url title
212+ fromInline (Image is url title) = CT.Image (fmap fromInline is) url title
213+ fromInline (Entity txt) = CT.Entity txt
214+ fromInline (RawHtml src) = CT.RawHtml src
215+
216+
217+-- | Annotate the code samples in a docstring
218+annotCode :: forall a b. (String -> b) -- ^ How to annotate code samples
219+ -> Docstring a
220+ -> Docstring b
221+annotCode annot (DocString opts blocks)
222+ = DocString opts $ fmap annotCodeBlock blocks
223+ where
224+ annotCodeBlock :: Block a -> Block b
225+ annotCodeBlock (Para inlines) = Para (fmap annotCodeInline inlines)
226+ annotCodeBlock (Header i inlines) = Header i (fmap annotCodeInline inlines)
227+ annotCodeBlock (Blockquote blocks) = Blockquote (fmap annotCodeBlock blocks)
228+ annotCodeBlock (List b t blocks) = List b t (fmap (fmap annotCodeBlock) blocks)
229+ annotCodeBlock (CodeBlock attrs src _) = CodeBlock attrs src (annot (T.unpack src))
230+ annotCodeBlock (HtmlBlock src) = HtmlBlock src
231+ annotCodeBlock HRule = HRule
232+
233+ annotCodeInline :: Inline a -> Inline b
234+ annotCodeInline (Str t) = Str t
235+ annotCodeInline Space = Space
236+ annotCodeInline SoftBreak = SoftBreak
237+ annotCodeInline LineBreak = LineBreak
238+ annotCodeInline (Emph is) = Emph (fmap annotCodeInline is)
239+ annotCodeInline (Strong is) = Strong (fmap annotCodeInline is)
240+ annotCodeInline (Code src _) = Code src (annot (T.unpack src))
241+ annotCodeInline (Link is url title) = Link (fmap annotCodeInline is) url title
242+ annotCodeInline (Image is url title) = Image (fmap annotCodeInline is) url title
243+ annotCodeInline (Entity txt) = Entity txt
244+ annotCodeInline (RawHtml src) = RawHtml src
src/Idris/Elab/Class.hs+2−2
@@ -52,9 +52,9 @@ import Util.Pretty(pretty, text)
5252
5353data MArgTy = IA | EA | CA deriving Show
5454
55−elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
55+elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->
5656 FC -> [PTerm] ->
57− Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()
57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Maybe PTerm))] -> [PDecl] -> Idris ()
5858elabClass info syn_in doc fc constraints tn ps pDocs ds
5959 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)
6060 let tty = pibind ps PType
src/Idris/Elab/Data.hs+16−9
@@ -20,6 +20,7 @@ import IRTS.Lang
2020
2121import Idris.Elab.Type
2222import Idris.Elab.Utils
23+import Idris.Elab.Value
2324
2425import Idris.Core.TT
2526import Idris.Core.Elaborate hiding (Tactic(..))
@@ -49,7 +50,7 @@ import Data.List.Split (splitOn)
4950
5051import Util.Pretty(pretty, text)
5152
52−elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
53+elabData :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] -> FC -> DataOpts -> PData -> Idris ()
5354elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
5455 = do let codata = Codata `elem` opts
5556 iLOG (show (fc, doc))
@@ -88,7 +89,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
8889 addIBC (IBCDef n)
8990 addIBC (IBCData n)
9091 checkDocs fc argDocs t
91− addDocStr n doc argDocs
92+ doc' <- elabDocTerms info doc
93+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
94+ return (n, d')) argDocs
95+ addDocStr n doc' argDocs'
9296 addIBC (IBCDoc n)
9397 let metainf = DataMI params
9498 addIBC (IBCMetaInformation n metainf)
@@ -207,7 +211,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
207211-- forcenames is probably no longer needed
208212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
209213 Type -> -- for kind checking
210− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->
214+ (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->
211215 Idris (Name, Type)
212216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
213217 = do checkUndefined fc n
@@ -225,7 +229,10 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
225229
226230 addIBC (IBCDef n)
227231 checkDocs fc argDocs t
228− addDocStr n doc argDocs
232+ doc' <- elabDocTerms info doc
233+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
234+ return (n, d')) argDocs
235+ addDocStr n doc' argDocs'
229236 addIBC (IBCDoc n)
230237 fputState (opt_inaccessible . ist_optimisation n) inacc
231238 addIBC (IBCOpt n)
@@ -274,7 +281,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris
274281-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
275282-- rename to caseFun to match updated intend
276283elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
277− [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
284+ [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])] ->
278285 ElabInfo -> EliminatorState ()
279286elabCaseFun ind paramPos n ty cons info = do
280287 elimLog $ "Elaborating case function"
@@ -293,7 +300,7 @@ elabCaseFun ind paramPos n ty cons info = do
293300 let motiveConstr = [(motiveName, expl, motive)]
294301 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
295302 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
296− let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
303+ let eliminatorTyDecl = PTy (fmap (const Nothing) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
297304 let clauseConsElimArgs = map getPiName consTerms
298305 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
299306 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
@@ -443,7 +450,7 @@ elabCaseFun ind paramPos n ty cons info = do
443450 splitArgPms _ = ([],[])
444451
445452
446− implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
453+ implicitIndexes :: (Docstring (Maybe PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
447454 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
448455 i <- State.lift getIState
449456 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -458,7 +465,7 @@ elabCaseFun ind paramPos n ty cons info = do
458465 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
459466 _ -> return implargs
460467
461− extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
468+ extractConsTerm :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
462469 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
463470 let cons' = replaceParams paramPos generalParameters ty
464471 let (args, resTy) = splitPi cons'
@@ -494,7 +501,7 @@ elabCaseFun ind paramPos n ty cons info = do
494501 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
495502 convertImplPi _ = Nothing
496503
497− generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
504+ generateEliminatorClauses :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
498505 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
499506 let cons' = replaceParams paramPos generalParameters ty
500507 let (args, resTy) = splitPi cons'
src/Idris/Elab/Provider.hs+1−1
@@ -98,7 +98,7 @@ elabProvider info syn fc what n
9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
9999 | ProvPostulate _ <- what ->
100100 do -- Add the postulate
101− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
101+ elabPostulate info syn (fmap (const Nothing) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
102102 logLvl 3 $ "Elaborated provided postulate " ++ show n
103103 | otherwise ->
104104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
src/Idris/Elab/Record.hs+2−2
@@ -50,8 +50,8 @@ import Data.List.Split (splitOn)
5050
5151import Util.Pretty(pretty, text)
5252
53−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
54− PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
53+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> FC -> Name ->
54+ PTerm -> DataOpts -> Docstring (Maybe PTerm) -> Name -> PTerm -> Idris ()
5555elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
5656 = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
5757 -- TODO think: something more in info?
src/Idris/Elab/Type.hs+15−6
@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2−module Idris.Elab.Type(buildType, elabType, elabType', elabPostulate) where
2+module Idris.Elab.Type (buildType, elabType, elabType', elabPostulate) where
33
44import Idris.AbsSyntax
55import Idris.ASTUtils
@@ -19,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
1919import IRTS.Lang
2020
2121import Idris.Elab.Utils
22+import Idris.Elab.Value
2223
2324import Idris.Core.TT
2425import Idris.Core.Elaborate hiding (Tactic(..))
@@ -27,7 +28,7 @@ import Idris.Core.Execute
2728import Idris.Core.Typecheck
2829import Idris.Core.CaseTree
2930
30−import Idris.Docstrings
31+import Idris.Docstrings (Docstring)
3132
3233import Prelude hiding (id, (.))
3334import Control.Category
@@ -40,6 +41,8 @@ import Data.List
4041import Data.Maybe
4142import Debug.Trace
4243
44+import qualified Data.Traversable as Traversable
45+
4346import qualified Data.Map as Map
4447import qualified Data.Set as S
4548import qualified Data.Text as T
@@ -111,12 +114,12 @@ buildType info syn fc opts n ty' = do
111114 param_pos i ns t = []
112115
113116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
114−elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
117+elabType :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] ->
115118 FC -> FnOpts -> Name -> PTerm -> Idris Type
116119elabType = elabType' False
117120
118121elabType' :: Bool -> -- normalise it
119− ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
122+ ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> [(Name, Docstring (Maybe PTerm))] ->
120123 FC -> FnOpts -> Name -> PTerm -> Idris Type
121124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
122125 n = liftname info n_in in -}
@@ -152,7 +155,10 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
152155 addDeferred ds'
153156 setFlags n opts'
154157 checkDocs fc argDocs ty
155− addDocStr n doc argDocs
158+ doc' <- elabDocTerms info doc
159+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
160+ return (n, d')) argDocs
161+ addDocStr n doc' argDocs'
156162 addIBC (IBCDoc n)
157163 addIBC (IBCFlags n opts')
158164 fputState (opt_inaccessible . ist_optimisation n) inacc
@@ -200,7 +206,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
200206 , ns4 == map txt ["Reflection","Language"] = True
201207 tyIsHandler _ = False
202208
203−elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
209+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->
204210 FC -> FnOpts -> Name -> PTerm -> Idris ()
205211elabPostulate info syn doc fc opts n ty = do
206212 elabType info syn doc [] fc opts n ty
@@ -209,3 +215,6 @@ elabPostulate info syn doc fc opts n ty = do
209215
210216 -- remove it from the deferred definitions list
211217 solveDeferred n
218+
219+
220+
src/Idris/Elab/Utils.hs+2−2
@@ -16,6 +16,7 @@ import Control.Applicative hiding (Const)
1616import Control.Monad.State
1717import Control.Monad
1818import Data.List
19+import qualified Data.Traversable as Traversable
1920
2021import Debug.Trace
2122
@@ -105,7 +106,7 @@ inferredDiff fc inf user =
105106-- | Check a PTerm against documentation and ensure that every documented
106107-- argument actually exists. This must be run _after_ implicits have been
107108-- found, or it will give spurious errors.
108−checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
109+checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
109110checkDocs fc args tm = cd (Map.fromList args) tm
110111 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
111112 cd as _ | Map.null as = return ()
@@ -235,4 +236,3 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []
235236 getUniqB env us b = getUniq env us (binderTy b)
236237
237238
238−
src/Idris/Elab/Value.hs+11−1
@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2−module Idris.Elab.Value(elabVal, elabValBind) where
2+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where
33
44import Idris.AbsSyntax
55import Idris.ASTUtils
@@ -38,6 +38,7 @@ import Control.Monad
3838import Control.Monad.State.Strict as State
3939import Data.List
4040import Data.Maybe
41+import qualified Data.Traversable as Traversable
4142import Debug.Trace
4243
4344import qualified Data.Map as Map
@@ -86,3 +87,12 @@ elabVal info aspat tm_in
8687 return (tm, ty)
8788
8889
90+
91+elabDocTerms :: ElabInfo -> Docstring (Maybe PTerm) -> Idris (Docstring (Maybe Term))
92+elabDocTerms info str = Traversable.mapM decorate str
93+ where decorate Nothing = return Nothing
94+ decorate (Just pt) = fmap (fmap fst) (tryElabVal info ERHS pt)
95+ tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Maybe (Term, Type))
96+ tryElabVal info aspat tm_in
97+ = idrisCatch (fmap Just $ elabVal info aspat tm_in)
98+ (const $ return Nothing)
src/Idris/IBC.hs+48−47
@@ -10,7 +10,8 @@ import Idris.AbsSyntax
1010import Idris.Imports
1111import Idris.Error
1212import Idris.Delaborate
13−import Idris.Docstrings
13+import qualified Idris.Docstrings as D
14+import Idris.Docstrings (Docstring)
1415import Idris.Output
1516
1617import qualified Cheapskate.Types as CT
@@ -31,7 +32,7 @@ import Codec.Compression.Zlib (compress)
3132import Util.Zlib (decompressEither)
3233
3334ibcVersion :: Word8
34−ibcVersion = 80
35+ibcVersion = 81
3536
3637data IBCFile = IBCFile { ver :: Word8,
3738 sourcefile :: FilePath,
@@ -60,7 +61,7 @@ data IBCFile = IBCFile { ver :: Word8,
6061 ibc_fninfo :: [(Name, FnInfo)],
6162 ibc_cg :: [(Name, CGInfo)],
6263 ibc_defs :: [(Name, Def)],
63− ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],
64+ ibc_docstrings :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))],
6465 ibc_transforms :: [(Term, Term)],
6566 ibc_errRev :: [(Term, Term)],
6667 ibc_coercions :: [Name],
@@ -458,7 +459,7 @@ pDefs syms ds
458459 update (Proj t i) = Proj (update t) i
459460 update t = t
460461
461−pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()
462+pDocs :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))] -> Idris ()
462463pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds
463464
464465pAccess :: [(Name, Accessibility)] -> Idris ()
@@ -521,13 +522,13 @@ pMetavars ns = do i <- getIState
521522 putIState $ i { idris_metavars = Data.List.reverse ns
522523 ++ idris_metavars i }
523524
524−----- For Cheapskate
525+----- For Cheapskate and docstrings
525526
526−instance Binary CT.Doc where
527− put (CT.Doc opts lines) = do put opts ; put lines
527+instance Binary a => Binary (D.Docstring a) where
528+ put (D.DocString opts lines) = do put opts ; put lines
528529 get = do opts <- get
529530 lines <- get
530− return (CT.Doc opts lines)
531+ return (D.DocString opts lines)
531532
532533instance Binary CT.Options where
533534 put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4
@@ -537,49 +538,49 @@ instance Binary CT.Options where
537538 x4 <- get
538539 return (CT.Options x1 x2 x3 x4)
539540
540−instance Binary CT.Block where
541− put (CT.Para lines) = do putWord8 0 ; put lines
542− put (CT.Header i lines) = do putWord8 1 ; put i ; put lines
543− put (CT.Blockquote bs) = do putWord8 2 ; put bs
544− put (CT.List b t xs) = do putWord8 3 ; put b ; put t ; put xs
545− put (CT.CodeBlock attr txt) = do putWord8 4 ; put attr ; put txt
546− put (CT.HtmlBlock txt) = do putWord8 5 ; put txt
547− put CT.HRule = putWord8 6
541+instance Binary a => Binary (D.Block a) where
542+ put (D.Para lines) = do putWord8 0 ; put lines
543+ put (D.Header i lines) = do putWord8 1 ; put i ; put lines
544+ put (D.Blockquote bs) = do putWord8 2 ; put bs
545+ put (D.List b t xs) = do putWord8 3 ; put b ; put t ; put xs
546+ put (D.CodeBlock attr txt src) = do putWord8 4 ; put attr ; put txt ; put src
547+ put (D.HtmlBlock txt) = do putWord8 5 ; put txt
548+ put D.HRule = putWord8 6
548549 get = do i <- getWord8
549550 case i of
550− 0 -> fmap CT.Para get
551− 1 -> liftM2 CT.Header get get
552− 2 -> fmap CT.Blockquote get
553− 3 -> liftM3 CT.List get get get
554− 4 -> liftM2 CT.CodeBlock get get
555− 5 -> liftM CT.HtmlBlock get
556− 6 -> return CT.HRule
557−
558−instance Binary CT.Inline where
559− put (CT.Str txt) = do putWord8 0 ; put txt
560− put CT.Space = putWord8 1
561− put CT.SoftBreak = putWord8 2
562− put CT.LineBreak = putWord8 3
563− put (CT.Emph xs) = putWord8 4 >> put xs
564− put (CT.Strong xs) = putWord8 5 >> put xs
565− put (CT.Code xs) = putWord8 6 >> put xs
566− put (CT.Link a b c) = putWord8 7 >> put a >> put b >> put c
567− put (CT.Image a b c) = putWord8 8 >> put a >> put b >> put c
568− put (CT.Entity a) = putWord8 9 >> put a
569− put (CT.RawHtml x) = putWord8 10 >> put x
551+ 0 -> fmap D.Para get
552+ 1 -> liftM2 D.Header get get
553+ 2 -> fmap D.Blockquote get
554+ 3 -> liftM3 D.List get get get
555+ 4 -> liftM3 D.CodeBlock get get get
556+ 5 -> liftM D.HtmlBlock get
557+ 6 -> return D.HRule
558+
559+instance Binary a => Binary (D.Inline a) where
560+ put (D.Str txt) = do putWord8 0 ; put txt
561+ put D.Space = putWord8 1
562+ put D.SoftBreak = putWord8 2
563+ put D.LineBreak = putWord8 3
564+ put (D.Emph xs) = putWord8 4 >> put xs
565+ put (D.Strong xs) = putWord8 5 >> put xs
566+ put (D.Code xs tm) = putWord8 6 >> put xs >> put tm
567+ put (D.Link a b c) = putWord8 7 >> put a >> put b >> put c
568+ put (D.Image a b c) = putWord8 8 >> put a >> put b >> put c
569+ put (D.Entity a) = putWord8 9 >> put a
570+ put (D.RawHtml x) = putWord8 10 >> put x
570571 get = do i <- getWord8
571572 case i of
572− 0 -> liftM CT.Str get
573− 1 -> return CT.Space
574− 2 -> return CT.SoftBreak
575− 3 -> return CT.LineBreak
576− 4 -> liftM CT.Emph get
577− 5 -> liftM CT.Strong get
578− 6 -> liftM CT.Code get
579− 7 -> liftM3 CT.Link get get get
580− 8 -> liftM3 CT.Image get get get
581− 9 -> liftM CT.Entity get
582− 10 -> liftM CT.RawHtml get
573+ 0 -> liftM D.Str get
574+ 1 -> return D.Space
575+ 2 -> return D.SoftBreak
576+ 3 -> return D.LineBreak
577+ 4 -> liftM D.Emph get
578+ 5 -> liftM D.Strong get
579+ 6 -> liftM2 D.Code get get
580+ 7 -> liftM3 D.Link get get get
581+ 8 -> liftM3 D.Image get get get
582+ 9 -> liftM D.Entity get
583+ 10 -> liftM D.RawHtml get
583584
584585instance Binary CT.ListType where
585586 put (CT.Bullet c) = putWord8 0 >> put c
src/Idris/IdrisDoc.hs+7−7
@@ -13,6 +13,7 @@ import Idris.ParseHelpers (opChars)
1313import Idris.AbsSyntax
1414import Idris.Docs
1515import Idris.Docstrings (nullDocstring)
16+import qualified Idris.Docstrings as Docstrings
1617
1718import IRTS.System (getDataFileName)
1819
@@ -37,7 +38,6 @@ import System.IO.Error
3738import System.FilePath
3839import System.Directory
3940
40−import Cheapskate.Html (renderDoc)
4141import Text.PrettyPrint.Annotated.Leijen (displayDecorated, renderCompact)
4242
4343import Text.Blaze (toValue, contents)
@@ -496,7 +496,7 @@ genTypeHeader ist (FD n _ args ftype _) = do
496496 docExtractor (_, _, _, Nothing) = Nothing
497497 docExtractor (n, _, _, Just d) = Just (n, doc2Str d)
498498 -- TODO: Remove <p> tags more robustly
499− doc2Str d = let dirty = renderMarkup $ contents $ renderDoc $ d
499+ doc2Str d = let dirty = renderMarkup $ contents $ Docstrings.renderHtml $ d
500500 in take (length dirty - 8) $ drop 3 dirty
501501
502502 name (NS n ns) = show (NS (sUN $ name n) ns)
@@ -523,7 +523,7 @@ createFunDoc :: IState -- ^ Needed to determine the types of names
523523createFunDoc ist fd@(FD name docstring args ftype fixity) = do
524524 H.dt ! (A.id $ toValue $ show name) $ genTypeHeader ist fd
525525 H.dd $ do
526− (if nullDocstring docstring then Empty else renderDoc docstring)
526+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)
527527 let args' = filter (\(_, _, _, d) -> isJust d) args
528528 if (not $ null args') || (isJust fixity)
529529 then H.dl $ do
@@ -546,7 +546,7 @@ createFunDoc ist fd@(FD name docstring args ftype fixity) = do
546546 genArg (_, _, _, Nothing) = Empty
547547 genArg (name, _, _, Just docstring) = do
548548 H.dt $ toHtml $ show name
549− H.dd $ renderDoc docstring
549+ H.dd $ Docstrings.renderHtml docstring
550550
551551
552552-- | Generates HTML documentation for any Docs type
@@ -564,7 +564,7 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do
564564 $ toHtml $ name $ nsroot n
565565 H.span ! class_ "signature" $ nbsp
566566 H.dd $ do
567− (if nullDocstring docstring then Empty else renderDoc docstring)
567+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)
568568 H.dl ! class_ "decls" $ forM_ fds (createFunDoc ist)
569569
570570 where name (NS n ns) = show (NS (sUN $ name n) ns)
@@ -578,7 +578,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do
578578 H.span ! class_ "word" $ do "data"; nbsp
579579 genTypeHeader ist fd
580580 H.dd $ do
581− (if nullDocstring docstring then Empty else renderDoc docstring)
581+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)
582582 let args' = filter (\(_, _, _, d) -> isJust d) args
583583 if not $ null args'
584584 then H.dl $ forM_ args' genArg
@@ -588,7 +588,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do
588588 where genArg (_, _, _, Nothing) = Empty
589589 genArg (name, _, _, Just docstring) = do
590590 H.dt $ toHtml $ show name
591− H.dd $ renderDoc docstring
591+ H.dd $ Docstrings.renderHtml docstring
592592
593593
594594-- | Generates everything but the actual content of the page
src/Idris/Output.hs+10
@@ -175,6 +175,16 @@ printUndefinedNames ns = text "Undefined " <> names <> text "."
175175 where names = encloseSep empty empty (char ',') $ map ppName ns
176176 ppName = prettyName True True []
177177
178+
179+prettyDocumentedIst :: IState
180+ -> (Name, PTerm, Maybe (Docstring (Maybe Term)))
181+ -> Doc OutputAnnotation
182+prettyDocumentedIst ist (name, ty, docs) =
183+ prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
184+ fromMaybe empty (fmap (\d -> renderDocstring ppTm d <> line) docs)
185+ where ppTm = pprintDelab ist
186+
187+
178188renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
179189renderExternal fmt width doc
180190 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."
src/Idris/ParseData.hs+27−13
@@ -42,25 +42,29 @@ Record ::=
4242 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
4343-}
4444record :: SyntaxInfo -> IdrisParser PDecl
45−record syn = do (doc, acc, opts) <- try (do
46− doc <- option noDocs docComment
45+record syn = do (doc, argDocs, acc, opts) <- try (do
46+ (doc, argDocs) <- option noDocs docComment
47+ ist <- get
48+ let doc' = annotCode (tryFullExpr syn ist) doc
49+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
50+ | (n, d) <- argDocs ]
4751 acc <- optional accessibility
4852 opts <- dataOpts []
4953 reserved "record"
50− return (doc, acc, opts))
54+ return (doc', argDocs', acc, opts))
5155 fc <- getFC
5256 tyn_in <- fnName
5357 lchar ':'
5458 ty <- typeExpr (allowImp syn)
5559 let tyn = expandNS syn tyn_in
5660 reserved "where"
57− (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)
61+ (cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)
5862 accData acc tyn [cn]
5963 let rsyn = syn { syn_namespace = show (nsroot tyn) :
6064 syn_namespace syn }
6165 let fns = getRecNames rsyn cty
6266 mapM_ (\n -> addAcc n acc) fns
63− return $ PRecord (fst doc) rsyn fc tyn ty opts cdoc cn cty
67+ return $ PRecord doc rsyn fc tyn ty opts cdoc cn cty
6468 <?> "record type declaration"
6569 where
6670 getRecNames :: SyntaxInfo -> PTerm -> [Name]
@@ -112,8 +116,12 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
112116 acc <- optional accessibility
113117 elim <- dataOpts []
114118 co <- dataI
115− let dataOpts = combineDataOpts(elim ++ co)
116− return (doc, argDocs, acc, dataOpts))
119+ ist <- get
120+ let dataOpts = combineDataOpts (elim ++ co)
121+ doc' = annotCode (tryFullExpr syn ist) doc
122+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
123+ | (n, d) <- argDocs ]
124+ return (doc', argDocs', acc, dataOpts))
117125 fc <- getFC
118126 tyn_in <- fnName
119127 (do try (lchar ':')
@@ -164,7 +172,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
164172{- | Parses a type constructor declaration
165173 Constructor ::= DocComment? FnName TypeSig;
166174-}
167−constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])
175+constructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])
168176constructor syn
169177 = do (doc, argDocs) <- option noDocs docComment
170178 cn_in <- fnName; fc <- getFC
@@ -175,21 +183,27 @@ constructor syn
175183 fs <- option [] (do lchar '%'; reserved "erase"
176184 sepBy1 name (lchar ','))
177185 ty <- typeExpr (allowImp syn)
178− return (doc, argDocs, cn, ty, fc, fs)
186+ ist <- get
187+ let doc' = annotCode (tryFullExpr syn ist) doc
188+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
189+ | (n, d) <- argDocs ]
190+ return (doc', argDocs', cn, ty, fc, fs)
179191 <?> "constructor"
180192
181−{- | Parses a constructor for simple discriminative union data types
193+{- | Parses a constructor for simple discriminated union data types
182194 SimpleConstructor ::= FnName SimpleExpr* DocComment?
183195-}
184−simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])
196+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, [PTerm], FC, [Name])
185197simpleConstructor syn
186− = do doc <- option noDocs (try docComment)
198+ = do (doc, _) <- option noDocs (try docComment)
199+ ist <- get
200+ let doc' = annotCode (tryFullExpr syn ist) doc
187201 cn_in <- fnName
188202 let cn = expandNS syn cn_in
189203 fc <- getFC
190204 args <- many (do notEndApp
191205 simpleExpr syn)
192− return (fst doc, [], cn, args, fc, [])
206+ return (doc', [], cn, args, fc, [])
193207 <?> "constructor"
194208
195209{- | Parses a dsl block declaration
src/Idris/ParseExpr.hs+6
@@ -53,6 +53,11 @@ fullExpr syn = do x <- expr syn
5353 i <- get
5454 return $ debindApp syn (desugar syn i x)
5555
56+tryFullExpr :: SyntaxInfo -> IState -> String -> Maybe PTerm
57+tryFullExpr syn st input =
58+ case runparser (fullExpr syn) st "" input of
59+ Success tm -> Just tm
60+ _ -> Nothing
5661
5762{- | Parses an expression
5863@
@@ -1325,3 +1330,4 @@ fullTactic :: SyntaxInfo -> IdrisParser PTactic
13251330fullTactic syn = do t <- tactic syn
13261331 eof
13271332 return t
1333+
src/Idris/ParseHelpers.hs+2−2
@@ -146,14 +146,14 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
146146 startEnd :: String
147147 startEnd = "{}-"
148148
149−{-| Parses a documentation comment (similar to haddoc) given a marker character
149+{-| Parses a documentation comment (similar to haddock) given a marker character
150150
151151@
152152 DocComment_t ::= '|||' ~EOL_t* EOL_t
153153 ;
154154@
155155 -}
156−docComment :: IdrisParser (Docstring, [(Name, Docstring)])
156+docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
157157docComment = do dc <- pushIndent *> docCommentLine
158158 rest <- many (indented docCommentLine)
159159 args <- many $ do (name, first) <- indented argDocCommentLine
src/Idris/Parser.hs+22−13
@@ -329,12 +329,15 @@ fnDecl syn = try (do notEndBlock
329329-}
330330fnDecl' :: SyntaxInfo -> IdrisParser PDecl
331331fnDecl' syn = checkFixity $
332− do (doc, fc, opts', n, acc) <- try (do
332+ do (doc, argDocs, fc, opts', n, acc) <- try (do
333333 pushIndent
334+ (doc, argDocs) <- option noDocs docComment
334335 ist <- get
335− doc <- option noDocs docComment
336− ist <- get
337− let initOpts = if default_total ist
336+ let doc' = annotCode (tryFullExpr syn ist) doc
337+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
338+ | (n, d) <- argDocs ]
339+
340+ initOpts = if default_total ist
338341 then [TotalFn]
339342 else []
340343 opts <- fnOpts initOpts
@@ -344,11 +347,11 @@ fnDecl' syn = checkFixity $
344347 let n = expandNS syn n_in
345348 fc <- getFC
346349 lchar ':'
347− return (doc, fc, opts', n, acc))
350+ return (doc', argDocs', fc, opts', n, acc))
348351 ty <- typeExpr (allowImp syn)
349352 terminator
350353 addAcc n acc
351− return (PTy (fst doc) (snd doc) syn fc opts' n ty)
354+ return (PTy doc argDocs syn fc opts' n ty)
352355 <|> postulate syn
353356 <|> caf syn
354357 <|> pattern syn
@@ -434,10 +437,12 @@ Postulate ::=
434437@
435438-}
436439postulate :: SyntaxInfo -> IdrisParser PDecl
437−postulate syn = do doc <- try $ do doc <- option noDocs docComment
440+postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment
441+ ist <- get
442+ let doc' = annotCode (tryFullExpr syn ist) doc
438443 pushIndent
439444 reserved "postulate"
440− return doc
445+ return doc'
441446 ist <- get
442447 let initOpts = if default_total ist
443448 then [TotalFn]
@@ -452,7 +457,7 @@ postulate syn = do doc <- try $ do doc <- option noDocs docComment
452457 fc <- getFC
453458 terminator
454459 addAcc n acc
455− return (PPostulate (fst doc) syn fc opts' n ty)
460+ return (PPostulate doc syn fc opts' n ty)
456461 <?> "postulate"
457462
458463{- | Parses a using declaration
@@ -581,16 +586,20 @@ Class ::=
581586@
582587-}
583588class_ :: SyntaxInfo -> IdrisParser [PDecl]
584−class_ syn = do (doc, acc) <- try (do
585− doc <- option noDocs docComment
589+class_ syn = do (doc, argDocs, acc) <- try (do
590+ (doc, argDocs) <- option noDocs docComment
591+ ist <- get
592+ let doc' = annotCode (tryFullExpr syn ist) doc
593+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)
594+ | (n, d) <- argDocs ]
586595 acc <- optional accessibility
587− return (doc, acc))
596+ return (doc', argDocs', acc))
588597 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
589598 let n = expandNS syn n_in
590599 cs <- many carg
591600 ds <- option [] (classBlock syn)
592601 accData acc n (concatMap declared ds)
593− return [PClass (fst doc) syn fc cons n cs (snd doc) ds]
602+ return [PClass doc syn fc cons n cs argDocs ds]
594603 <?> "type-class declaration"
595604 where
596605 carg :: IdrisParser (Name, PTerm)
src/Idris/TypeSearch.hs+2−2
@@ -23,14 +23,14 @@ import Data.Traversable (traverse)
2323import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)
2424import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,
2525 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
26− implicitAllowed, OutputMode(..), prettyDocumentedIst, PTerm, toplevel)
26+ implicitAllowed, OutputMode(..), PTerm, toplevel)
2727import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
2828import Idris.Core.TT hiding (score)
2929import Idris.Core.Unify (match_unify)
3030import Idris.Delaborate (delabTy)
3131import Idris.Docstrings (noDocs, overview)
3232import Idris.Elab.Type (elabType)
33−import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)
33+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult, prettyDocumentedIst)
3434
3535import Prelude hiding (pred)
3636