e90316a · Idris-dev · git.iko.soy

CHANGELOG+2

@@ -28,6 +28,8 @@ New in 0.9.15:

2828 documentation lookups, and with semantic highlighting for IDEs.

2929* Fenced code blocks in docs defined with the "example" attribute are rendered

3030 as code examples.

31+* Fenced code blocks declared to be Idris code that fail to parse or type check now

32+ provide error messages to IDE clients.

3133* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

3234 Engine style)

3335

idris.cabal+1−1

@@ -692,7 +692,7 @@ Library

692692 , ansi-terminal < 0.7

693693 , ansi-wl-pprint < 0.7

694694 , base64-bytestring < 1.1

695− , binary < 0.8

695+ , binary >= 0.7 && < 0.8

696696 , blaze-html >= 0.6.1.3 && < 0.8

697697 , blaze-markup >= 0.5.2.1 && < 0.7.0.0

698698 , bytestring < 0.11

src/Idris/AbsSyntax.hs+1−1

@@ -286,7 +286,7 @@ addCoercion :: Name -> Idris ()

286286addCoercion n = do i <- getIState

287287 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

288288

289−addDocStr :: Name -> Docstring (Maybe Term) -> [(Name, Docstring (Maybe Term))] -> Idris ()

289+addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()

290290addDocStr n doc args

291291 = do i <- getIState

292292 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

src/Idris/AbsSyntaxTree.hs+16−15

@@ -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 (Maybe Term), [(Name, Docstring (Maybe Term))]),

161+ idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),

162162 idris_tyinfodata :: Ctxt TIData,

163163 idris_fninfo :: Ctxt FnInfo,

164164 idris_transforms :: Ctxt [(Term, Term)],

@@ -536,19 +536,19 @@ type ProvideWhat = ProvideWhat' PTerm

536536-- datatypes and typeclasses.

537537data PDecl' t

538538 = PFix FC Fixity [String] -- ^ Fixity declaration

539− | PTy (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

540− | PPostulate (Docstring (Maybe PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

539+ | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

540+ | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

541541 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

542542 | PCAF FC Name t -- ^ Top level constant

543− | PData (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

543+ | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

544544 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

545545 | PNamespace String [PDecl' t] -- ^ New namespace

546− | PRecord (Docstring (Maybe PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Maybe PTerm)) Name t -- ^ Record declaration

547− | PClass (Docstring (Maybe PTerm)) SyntaxInfo FC

546+ | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration

547+ | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

548548 [t] -- constraints

549549 Name

550550 [(Name, t)] -- parameters

551− [(Name, Docstring (Maybe PTerm))] -- parameter docstrings

551+ [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

552552 [PDecl' t] -- declarations

553553 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

554554 -- class name, parameters, method declarations

@@ -599,7 +599,7 @@ deriving instance NFData PClause'

599599-- | Data declaration

600600data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

601601 d_tcon :: t, -- ^ Type constructor

602− d_cons :: [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, t, FC, [Name])] -- ^ Constructors

602+ d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors

603603 }

604604 -- ^ Data declaration

605605 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -1079,7 +1079,7 @@ unitTy = sUN "Unit"

10791079unitCon = sUN "MkUnit"

10801080

10811081-- TODO: elaborate the code samples in the docstring

1082−falseDoc = fmap (const Nothing) . parseDocstring . T.pack $

1082+falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $

10831083 "The empty type, also known as the trivially false proposition." ++

10841084 "\n\n" ++

10851085 "Use `void` or `absurd` to prove anything if you have a variable " ++

@@ -1091,7 +1091,7 @@ pairCon = sUN "MkPair"

10911091

10921092eqTy = sUN "="

10931093eqCon = sUN "Refl"

1094−eqDoc = fmap (const Nothing) . parseDocstring . T.pack $

1094+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

10951095 "The propositional equality type. A proof that `x` = `y`." ++

10961096 "\n\n" ++

10971097 "To use such a proof, pattern-match on it, and the two equal things will " ++

@@ -1114,14 +1114,14 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

11141114 pexp (PRef bi (n "x")),

11151115 pexp (PRef bi (n "x"))])), bi, [])]

11161116 where n a = sUN a

1117− reflDoc = annotCode (const Nothing) . parseDocstring . T.pack $

1117+ reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $

11181118 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

11191119 "shown that both sides are in fact equal."

1120− reflParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type at which the equality is proven"),

1121− (n "x", annotCode (const Nothing) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1120+ reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),

1121+ (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]

11221122

1123−eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left side of the equality"),

1124− (n "B", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")

1123+eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),

1124+ (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")

11251125 ]

11261126 where n a = sUN a

11271127

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

11881188 colour ItalicText = IdrisColour Nothing True False False True

11891189consoleDecorate ist (AnnTerm _ _) = id

11901190consoleDecorate ist (AnnSearchResult _) = id

1191+consoleDecorate ist (AnnErr _) = id

11911192

11921193isPostulateName :: Name -> IState -> Bool

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

src/Idris/Core/TT.hs+2−1

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

103103 | AnnTextFmt TextFormatting

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

105105 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific

106+ | AnnErr Err

106107

107108-- | Used for error reflection

108109data ErrorReportPart = TextPart String

@@ -117,7 +118,7 @@ data ErrorReportPart = TextPart String

117118

118119-- | Idris errors. Used as exceptions in the compiler, but reported to users

119120-- if they reach the top level.

120−data Err' t

121+data Err' t

121122 = Msg String

122123 | InternalMsg String

123124 | CantUnify Bool t t (Err' t) [(Name, t)] Int

src/Idris/Delaborate.hs+6−4

@@ -9,7 +9,7 @@ import Util.Pretty

99import Idris.AbsSyntax

1010import Idris.Core.TT

1111import Idris.Core.Evaluate

12−import Idris.Docstrings (overview, renderDocstring)

12+import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

1313import Idris.ErrReverse

1414

1515import Data.List (intersperse, nub)

@@ -435,12 +435,14 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

435435 _ | otherwise -> annot

436436 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

437437 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

438− let o = overview (fst docs)

438+ let o = overview (fst docs)

439+ norm = normaliseAll (tt_ctxt ist) []

439440 -- TODO make width configurable

440441 -- Issue #1588 on the Issue Tracker

441442 -- https://github.com/idris-lang/Idris-dev/issues/1588

442− out = displayS . renderPretty 1.0 50 $

443− renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) o

443+ out = displayS . renderPretty 1.0 50 $

444+ renderDocstring (renderDocTerm (pprintDelab ist)

445+ norm) o

444446 return (out "")

445447 getTy :: IState -> Name -> String -- fails if name not already extant!

446448 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

src/Idris/Docs.hs+12−12

@@ -6,7 +6,7 @@ import Idris.AbsSyntaxTree

66import Idris.Delaborate

77import Idris.Core.TT

88import Idris.Core.Evaluate

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

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

1010

1111import Util.Pretty

1212

@@ -18,31 +18,31 @@ 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 (Maybe Term))

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

21+data FunDoc = FD Name (Docstring DocTerm)

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

2323 PTerm -- function type

2424 (Maybe Fixity)

25− deriving Show

2625

2726data Docs = FunDoc FunDoc

2827 | DataDoc FunDoc -- type constructor docs

2928 [FunDoc] -- data constructor docs

30− | ClassDoc Name (Docstring (Maybe Term))-- class docs

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

3130 [FunDoc] -- method docs

32− [(Name, Maybe (Docstring (Maybe Term)))] -- parameters and their docstrings

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

3332 [PTerm] -- instances

3433 [PTerm] -- superclasses

35− deriving Show

3634

37−showDoc ist d | nullDocstring d = empty

38− | otherwise = text " -- " <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) d

35+showDoc ist d

36+ | nullDocstring d = empty

37+ | otherwise = text " -- " <>

38+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d

3939

4040pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

4141pprintFD ist (FD n doc args ty f)

4242 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

4343 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

4444 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

45− renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc <$>

45+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>

4646 maybe empty (\f -> text (show f) <> line) f <>

4747 let argshow = showArgs args [] in

4848 if not (null argshow)

@@ -84,7 +84,7 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

8484 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

8585 if nullDocstring doc

8686 then empty

87− else line <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc)

87+ else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

8888 <> line <$>

8989 nest 4 (text "Parameters:" <$> prettyParameters)

9090 <> line <$>

@@ -187,7 +187,7 @@ docFun n

187187 funName (UN n) = str n

188188 funName (NS n _) = funName n

189189

190−getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]

190+getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]

191191getPArgNames (PPi plicity name ty body) ds =

192192 (name, ty, plicity, lookup name ds) : getPArgNames body ds

193193getPArgNames _ _ = []

src/Idris/Docstrings.hs+79−39

@@ -1,10 +1,10 @@

11{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

2−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

33

44-- | Wrapper around Markdown library

55module Idris.Docstrings (

66 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,

7− overview, containsText, renderHtml, annotCode

7+ overview, containsText, renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring

88 ) where

99

1010import qualified Cheapskate as C

@@ -13,7 +13,7 @@ import Cheapskate.Html (renderDoc)

1313

1414import Util.Pretty

1515

16−import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term)

16+import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)

1717

1818import qualified Data.Text as T

1919import qualified Data.Foldable as F

@@ -25,6 +25,22 @@ import Control.DeepSeq (NFData(..))

2525

2626import Text.Blaze.Html (Html)

2727

28+-- | The various kinds of code samples that can be embedded in docs

29+data DocTerm = Unchecked

30+ | Checked Term

31+ | Example Term

32+ | Failing Err

33+ deriving Show

34+

35+-- | Render a term in the documentation

36+renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation

37+renderDocTerm pp norm Unchecked src = text src

38+renderDocTerm pp norm (Checked tm) src = pp tm

39+renderDocTerm pp norm (Example tm) src = align $

40+ text ">" <+> align (pp tm) <$>

41+ pp (norm tm)

42+renderDocTerm pp norm (Failing err) src = annotate (AnnErr err) $ text src

43+

2844-- | Representation of Idris's inline documentation. The type paramter

2945-- represents the type of terms that are associated with code blocks.

3046data Docstring a = DocString CT.Options (Blocks a)

@@ -58,6 +74,37 @@ data Inline a = Str T.Text

5874type Inlines a = S.Seq (Inline a)

5975

6076

77+-- | Run some kind of processing step over code in a Docstring. The code

78+-- processor gets the language and annotations as parameters, along with the

79+-- source and the original annotation.

80+checkDocstring :: forall a b. (String -> [String] -> String -> a -> b) -> Docstring a -> Docstring b

81+checkDocstring f (DocString opts blocks) = DocString opts (fmap (checkBlock f) blocks)

82+ where checkBlock :: (String -> [String] -> String -> a -> b) -> Block a -> Block b

83+ checkBlock f (Para inlines) = Para (fmap (checkInline f) inlines)

84+ checkBlock f (Header i inlines) = Header i (fmap (checkInline f) inlines)

85+ checkBlock f (Blockquote bs) = Blockquote (fmap (checkBlock f) bs)

86+ checkBlock f (List b t blocks) = List b t (fmap (fmap (checkBlock f)) blocks)

87+ checkBlock f (CodeBlock attrs src tm) = CodeBlock attrs src

88+ (f (T.unpack $ CT.codeLang attrs)

89+ (words . T.unpack $ CT.codeInfo attrs)

90+ (T.unpack src)

91+ tm)

92+ checkBlock f (HtmlBlock src) = HtmlBlock src

93+ checkBlock f HRule = HRule

94+

95+ checkInline :: (String -> [String] -> String -> a -> b) -> Inline a -> Inline b

96+ checkInline f (Str txt) = Str txt

97+ checkInline f Space = Space

98+ checkInline f SoftBreak = SoftBreak

99+ checkInline f LineBreak = LineBreak

100+ checkInline f (Emph is) = Emph (fmap (checkInline f) is)

101+ checkInline f (Strong is) = Strong (fmap (checkInline f) is)

102+ checkInline f (Code src x) = Code src (f "" [] (T.unpack src) x)

103+ checkInline f (Link is url title) = Link (fmap (checkInline f) is) url title

104+ checkInline f (Image is url title) = Image (fmap (checkInline f) is) url title

105+ checkInline f (Entity txt) = Entity txt

106+ checkInline f (RawHtml src) = RawHtml src

107+

61108-- | Construct a docstring from a Text that contains Markdown-formatted docs

62109parseDocstring :: T.Text -> Docstring ()

63110parseDocstring = toDocstring . C.markdown options

@@ -94,60 +141,53 @@ options = CT.Options { CT.sanitize = True

94141 }

95142

96143-- | Convert a docstring to be shown by the pretty-printer

97−renderDocstring :: (a -> Doc OutputAnnotation) -> (a -> a) -> Docstring (Maybe a) -> Doc OutputAnnotation

98−renderDocstring pp norm (DocString _ blocks) = renderBlocks pp norm blocks

144+renderDocstring :: (a -> String -> Doc OutputAnnotation) -> Docstring a -> Doc OutputAnnotation

145+renderDocstring pp (DocString _ blocks) = renderBlocks pp blocks

99146

100147-- | Construct a docstring consisting of the first block-level element of the

101148-- argument docstring, for use in summaries.

102149overview :: Docstring a -> Docstring a

103150overview (DocString opts blocks) = DocString opts (S.take 1 blocks)

104151

105−renderBlocks :: (a -> Doc OutputAnnotation) -> (a -> a)

106− -> Blocks (Maybe a) -> Doc OutputAnnotation

107−renderBlocks pp norm blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

108− fmap (renderBlock pp norm) blocks

109− | S.length blocks == 1 = renderBlock pp norm (S.index blocks 0)

152+renderBlocks :: (a -> String -> Doc OutputAnnotation)

153+ -> Blocks a -> Doc OutputAnnotation

154+renderBlocks pp blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

155+ fmap (renderBlock pp) blocks

156+ | S.length blocks == 1 = renderBlock pp (S.index blocks 0)

110157 | otherwise = empty

111158

112−renderBlock :: (a -> Doc OutputAnnotation) -> (a -> a)

113− -> Block (Maybe a) -> Doc OutputAnnotation

114−renderBlock pp norm (Para inlines) = renderInlines pp inlines

115−renderBlock pp norm (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

116−renderBlock pp norm (Blockquote blocks) = indent 8 $ renderBlocks pp norm blocks

117−renderBlock pp norm (List b ty blockss) = renderList pp norm b ty blockss

118−renderBlock pp norm (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)

119−renderBlock pp norm (CodeBlock attr src (Just tm))

120− | isExample attr = indent 4 $

121− text ">" <+> align (group (pp tm)) <$>

122− align (group (pp (norm tm)))

123− | otherwise = indent 4 $ pp tm

124− where isExample (CT.CodeAttr lang info) = T.pack "example" `elem` lang : T.words info

125−renderBlock pp norm (HtmlBlock txt) = text "<html block>" -- TODO

126−renderBlock pp norm HRule = text "----------------------"

127−

128−renderList :: (a -> Doc OutputAnnotation) -> (a -> a)

129− -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation

130−renderList pp norm b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp norm) blockss

131−renderList pp norm b (CT.Numbered nw i) blockss =

159+renderBlock :: (a -> String -> Doc OutputAnnotation)

160+ -> Block a -> Doc OutputAnnotation

161+renderBlock pp (Para inlines) = renderInlines pp inlines

162+renderBlock pp (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

163+renderBlock pp (Blockquote blocks) = indent 8 $ renderBlocks pp blocks

164+renderBlock pp (List b ty blockss) = renderList pp b ty blockss

165+renderBlock pp (CodeBlock attr src tm) = indent 4 $ pp tm (T.unpack src)

166+renderBlock pp (HtmlBlock txt) = text "<html block>" -- TODO

167+renderBlock pp HRule = text "----------------------"

168+

169+renderList :: (a -> String -> Doc OutputAnnotation)

170+ -> Bool -> CT.ListType -> [Blocks a] -> Doc OutputAnnotation

171+renderList pp b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp) blockss

172+renderList pp b (CT.Numbered nw i) blockss =

132173 vsep $

133174 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

134− [i..] (repeat punc) (map (renderBlocks pp norm) blockss)

175+ [i..] (repeat punc) (map (renderBlocks pp) blockss)

135176 where punc = case nw of

136177 CT.PeriodFollowing -> char '.'

137178 CT.ParenFollowing -> char '('

138179

139−renderInlines :: (a -> Doc OutputAnnotation) -> Inlines (Maybe a) -> Doc OutputAnnotation

180+renderInlines :: (a -> String -> Doc OutputAnnotation) -> Inlines a -> Doc OutputAnnotation

140181renderInlines pp = F.foldr (<>) empty . fmap (renderInline pp)

141182

142−renderInline :: (a -> Doc OutputAnnotation) -> Inline (Maybe a) -> Doc OutputAnnotation

183+renderInline :: (a -> String -> Doc OutputAnnotation) -> Inline a -> Doc OutputAnnotation

143184renderInline pp (Str s) = text $ T.unpack s

144185renderInline pp Space = softline

145186renderInline pp SoftBreak = softline

146187renderInline pp LineBreak = line

147188renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt

148189renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt

149−renderInline pp (Code txt Nothing) = text $ T.unpack txt

150−renderInline pp (Code txt (Just tm)) = pp tm

190+renderInline pp (Code txt tm) = pp tm $ T.unpack txt

151191renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>

152192 parens (text $ T.unpack url)

153193renderInline pp (Image body url title) = text "<image>" -- TODO

@@ -193,13 +233,13 @@ containsText str (DocString _ blocks) = F.any (blockContains (T.toLower str)) bl

193233 inlineContains str (RawHtml txt) = T.isInfixOf str (T.toLower txt)

194234

195235

196−renderHtml :: Docstring (Maybe Term) -> Html

236+renderHtml :: Docstring DocTerm -> Html

197237renderHtml = renderDoc . fromDocstring

198238 where

199− fromDocstring :: Docstring (Maybe Term) -> CT.Doc

239+ fromDocstring :: Docstring DocTerm -> CT.Doc

200240 fromDocstring (DocString opts blocks) = CT.Doc opts (fmap fromBlock blocks)

201241

202− fromBlock :: Block (Maybe Term) -> CT.Block

242+ fromBlock :: Block DocTerm -> CT.Block

203243 fromBlock (Para inlines) = CT.Para (fmap fromInline inlines)

204244 fromBlock (Header i inlines) = CT.Header i (fmap fromInline inlines)

205245 fromBlock (Blockquote blocks) = CT.Blockquote (fmap fromBlock blocks)

@@ -208,7 +248,7 @@ renderHtml = renderDoc . fromDocstring

208248 fromBlock (HtmlBlock src) = CT.HtmlBlock src

209249 fromBlock HRule = CT.HRule

210250

211− fromInline :: Inline (Maybe Term) -> CT.Inline

251+ fromInline :: Inline DocTerm -> CT.Inline

212252 fromInline (Str t) = CT.Str t

213253 fromInline Space = CT.Space

214254 fromInline SoftBreak = CT.SoftBreak

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 (Maybe PTerm) ->

55+elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

5656 FC -> [PTerm] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Maybe PTerm))] -> [PDecl] -> Idris ()

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err 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/Clause.hs+1−1

@@ -30,7 +30,7 @@ import Idris.Core.Execute

3030import Idris.Core.Typecheck

3131import Idris.Core.CaseTree

3232

33−import Idris.Docstrings

33+import Idris.Docstrings hiding (Unchecked)

3434import Util.Pretty hiding ((<$>))

3535

3636import Prelude hiding (id, (.))

src/Idris/Elab/Data.hs+8−8

@@ -50,7 +50,7 @@ import Data.List.Split (splitOn)

5050

5151import Util.Pretty(pretty, text)

5252

53−elabData :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] -> FC -> DataOpts -> PData -> Idris ()

53+elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

5454elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

5555 = do let codata = Codata `elem` opts

5656 iLOG (show (fc, doc))

@@ -78,7 +78,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

7878 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

7979 ttag <- getName

8080 i <- getIState

81− let as = map (const Nothing) (getArgTys cty)

81+ let as = map (const (Left (Msg ""))) (getArgTys cty)

8282 let params = findParams (map snd cons)

8383 logLvl 2 $ "Parameters : " ++ show params

8484 -- TI contains information about mutually declared types - this will

@@ -206,7 +206,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

206206

207207elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

208208 Type -> -- for kind checking

209− (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->

209+ (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

210210 Idris (Name, Type)

211211elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

212212 = do checkUndefined fc n

@@ -279,7 +279,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris

279279-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

280280-- rename to caseFun to match updated intend

281281elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

282− [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])] ->

282+ [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])] ->

283283 ElabInfo -> EliminatorState ()

284284elabCaseFun ind paramPos n ty cons info = do

285285 elimLog $ "Elaborating case function"

@@ -298,7 +298,7 @@ elabCaseFun ind paramPos n ty cons info = do

298298 let motiveConstr = [(motiveName, expl, motive)]

299299 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

300300 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

301− let eliminatorTyDecl = PTy (fmap (const Nothing) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

301+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

302302 let clauseConsElimArgs = map getPiName consTerms

303303 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

304304 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -448,7 +448,7 @@ elabCaseFun ind paramPos n ty cons info = do

448448 splitArgPms _ = ([],[])

449449

450450

451− implicitIndexes :: (Docstring (Maybe PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

451+ implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

452452 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

453453 i <- State.lift getIState

454454 implargs' <- case lookupCtxt cnm (idris_implicits i) of

@@ -463,7 +463,7 @@ elabCaseFun ind paramPos n ty cons info = do

463463 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

464464 _ -> return implargs

465465

466− extractConsTerm :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

466+ extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

467467 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

468468 let cons' = replaceParams paramPos generalParameters ty

469469 let (args, resTy) = splitPi cons'

@@ -499,7 +499,7 @@ elabCaseFun ind paramPos n ty cons info = do

499499 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

500500 convertImplPi _ = Nothing

501501

502− generateEliminatorClauses :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

502+ generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

503503 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

504504 let cons' = replaceParams paramPos generalParameters ty

505505 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 (fmap (const Nothing) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

101+ elabPostulate info syn (fmap (const (Left $ Msg "")) . 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 (Maybe PTerm) -> FC -> Name ->

54− PTerm -> DataOpts -> Docstring (Maybe PTerm) -> Name -> PTerm -> Idris ()

53+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> Name ->

54+ PTerm -> DataOpts -> Docstring (Either Err 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+3−3

@@ -114,12 +114,12 @@ buildType info syn fc opts n ty' = do

114114 param_pos i ns t = []

115115

116116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] ->

117+elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

118118 FC -> FnOpts -> Name -> PTerm -> Idris Type

119119elabType = elabType' False

120120

121121elabType' :: Bool -> -- normalise it

122− ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> [(Name, Docstring (Maybe PTerm))] ->

122+ ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

123123 FC -> FnOpts -> Name -> PTerm -> Idris Type

124124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125125 n = liftname info n_in in -}

@@ -207,7 +207,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

207207 , ns4 == map txt ["Reflection","Language"] = True

208208 tyIsHandler _ = False

209209

210−elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

210+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

211211 FC -> FnOpts -> Name -> PTerm -> Idris ()

212212elabPostulate info syn doc fc opts n ty = do

213213 elabType info syn doc [] fc opts n ty

src/Idris/Elab/Value.hs+21−8

@@ -1,4 +1,5 @@

11{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

23module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

34

45import Idris.AbsSyntax

@@ -22,7 +23,7 @@ import Idris.Elab.Utils

2223

2324import Idris.Core.TT

2425import Idris.Core.Elaborate hiding (Tactic(..))

25−import Idris.Core.Evaluate

26+import Idris.Core.Evaluate hiding (Unchecked)

2627import Idris.Core.Execute

2728import Idris.Core.Typecheck

2829import Idris.Core.CaseTree

@@ -88,11 +89,23 @@ elabVal info aspat tm_in

8889

8990

9091

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

92+elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)

93+elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

94+ return $ checkDocstring mkDocTerm typechecked

95+ where decorate (Left err) = return (Left err)

96+ decorate (Right pt) = fmap (fmap fst) (tryElabVal info ERHS pt)

97+

98+ tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Either Err (Term, Type))

9699 tryElabVal info aspat tm_in

97− = idrisCatch (fmap Just $ elabVal info aspat tm_in)

98− (const $ return Nothing)

100+ = idrisCatch (fmap Right $ elabVal info aspat tm_in)

101+ (return . Left)

102+

103+ mkDocTerm :: String -> [String] -> String -> Either Err Term -> DocTerm

104+ mkDocTerm lang attrs src (Left err)

105+ | map toLower lang == "idris" = Failing err

106+ | otherwise = Unchecked

107+ mkDocTerm lang attrs src (Right tm)

108+ | map toLower lang == "idris" = if "example" `elem` map (map toLower) attrs

109+ then Example tm

110+ else Checked tm

111+ | otherwise = Unchecked

src/Idris/ElabDecls.hs+1−1

@@ -38,7 +38,7 @@ import Idris.Core.Execute

3838import Idris.Core.Typecheck

3939import Idris.Core.CaseTree

4040

41−import Idris.Docstrings

41+import Idris.Docstrings hiding (Unchecked)

4242

4343import Prelude hiding (id, (.))

4444import Control.Category

src/Idris/IBC.hs+17−3

@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)

3232import Util.Zlib (decompressEither)

3333

3434ibcVersion :: Word8

35−ibcVersion = 83

35+ibcVersion = 84

3636

3737data IBCFile = IBCFile { ver :: Word8,

3838 sourcefile :: FilePath,

@@ -61,7 +61,7 @@ data IBCFile = IBCFile { ver :: Word8,

6161 ibc_fninfo :: [(Name, FnInfo)],

6262 ibc_cg :: [(Name, CGInfo)],

6363 ibc_defs :: [(Name, Def)],

64− ibc_docstrings :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))],

64+ ibc_docstrings :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

6565 ibc_transforms :: [(Name, (Term, Term))],

6666 ibc_errRev :: [(Term, Term)],

6767 ibc_coercions :: [Name],

@@ -459,7 +459,7 @@ pDefs syms ds

459459 update (Proj t i) = Proj (update t) i

460460 update t = t

461461

462−pDocs :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))] -> Idris ()

462+pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

463463pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

464464

465465pAccess :: [(Name, Accessibility)] -> Idris ()

@@ -538,6 +538,20 @@ instance Binary CT.Options where

538538 x4 <- get

539539 return (CT.Options x1 x2 x3 x4)

540540

541+instance Binary D.DocTerm where

542+ put D.Unchecked = putWord8 0

543+ put (D.Checked t) = putWord8 1 >> put t

544+ put (D.Example t) = putWord8 2 >> put t

545+ put (D.Failing e) = putWord8 3 >> put e

546+

547+ get = do i <- getWord8

548+ case i of

549+ 0 -> return D.Unchecked

550+ 1 -> fmap D.Checked get

551+ 2 -> fmap D.Example get

552+ 3 -> fmap D.Failing get

553+ _ -> error "Corrupted binary data for DocTerm"

554+

541555instance Binary a => Binary (D.Block a) where

542556 put (D.Para lines) = do putWord8 0 ; put lines

543557 put (D.Header i lines) = do putWord8 1 ; put i ; put lines

src/Idris/IdeSlave.hs+13

@@ -1,3 +1,5 @@

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2+

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

24

35module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

@@ -151,6 +153,7 @@ instance SExpable OutputAnnotation where

151153 EQ -> "isomorphic"

152154 LT -> "more general than searched type"

153155 GT -> "more specific than searched type"

156+ toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]

154157

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

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

@@ -159,6 +162,12 @@ encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encod

159162decodeTerm :: String -> ([(Name, Bool)], Term)

160163decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

161164

165+encodeErr :: Err -> String

166+encodeErr e = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ e

167+

168+decodeErr :: String -> Err

169+decodeErr = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

170+

162171instance SExpable FC where

163172 toSExp (FC f (sl, sc) (el, ec)) =

164173 toSExp ((SymbolAtom "filename", StringAtom f),

@@ -219,6 +228,8 @@ data IdeSlaveCommand = REPLCompletions String

219228 | TermShowImplicits [(Name, Bool)] Term

220229 | TermNoImplicits [(Name, Bool)] Term

221230 | PrintDef String

231+ | ErrString Err

232+ | ErrPPrint Err

222233

223234sexpToCommand :: SExp -> Maybe IdeSlaveCommand

224235sexpToCommand (SexpList (x:[])) = sexpToCommand x

@@ -262,6 +273,8 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])

262273sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

263274 Just (TermNoImplicits bnd tm)

264275sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

276+sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

277+sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

265278sexpToCommand _ = Nothing

266279

267280parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/Output.hs+6−3

@@ -1,4 +1,4 @@

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

22

33module Idris.Output where

44

@@ -177,12 +177,13 @@ printUndefinedNames ns = text "Undefined " <> names <> text "."

177177

178178

179179prettyDocumentedIst :: IState

180− -> (Name, PTerm, Maybe (Docstring (Maybe Term)))

180+ -> (Name, PTerm, Maybe (Docstring DocTerm))

181181 -> Doc OutputAnnotation

182182prettyDocumentedIst ist (name, ty, docs) =

183183 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

184− fromMaybe empty (fmap (\d -> renderDocstring ppTm (normaliseAll (tt_ctxt ist) []) d <> line) docs)

184+ fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)

185185 where ppTm = pprintDelab ist

186+ norm = normaliseAll (tt_ctxt ist) []

186187

187188

188189renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

@@ -220,6 +221,7 @@ renderExternal fmt width doc

220221 decorate HTMLOutput (AnnTextFmt _) = id -- TODO

221222 decorate HTMLOutput (AnnTerm _ _) = id

222223 decorate HTMLOutput (AnnSearchResult _) = id

224+ decorate HTMLOutput (AnnErr _) = id

223225

224226 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

225227 latex "IdrisType"

@@ -242,6 +244,7 @@ renderExternal fmt width doc

242244 decorate LaTeXOutput (AnnTextFmt _) = id -- TODO

243245 decorate LaTeXOutput (AnnTerm _ _) = id

244246 decorate LaTeXOutput (AnnSearchResult _) = id

247+ decorate LaTeXOutput (AnnErr _) = id

245248

246249 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

247250 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

src/Idris/ParseData.hs+3−3

@@ -4,7 +4,7 @@ module Idris.ParseData where

44import Prelude hiding (pi)

55

66import Text.Trifecta.Delta

7−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

88import Text.Parser.LookAhead

99import Text.Parser.Expression

1010import qualified Text.Parser.Token as Tok

@@ -172,7 +172,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

172172{- | Parses a type constructor declaration

173173 Constructor ::= DocComment? FnName TypeSig;

174174-}

175−constructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])

175+constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])

176176constructor syn

177177 = do (doc, argDocs) <- option noDocs docComment

178178 cn_in <- fnName; fc <- getFC

@@ -191,7 +191,7 @@ constructor syn

191191{- | Parses a constructor for simple discriminated union data types

192192 SimpleConstructor ::= FnName SimpleExpr* DocComment?

193193-}

194−simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, [PTerm], FC, [Name])

194+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, [PTerm], FC, [Name])

195195simpleConstructor syn

196196 = do (doc, _) <- option noDocs (try docComment)

197197 ist <- get

src/Idris/ParseExpr.hs+4−4

@@ -5,7 +5,7 @@ module Idris.ParseExpr where

55import Prelude hiding (pi)

66

77import Text.Trifecta.Delta

8−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

8+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

99import Text.Parser.LookAhead

1010import Text.Parser.Expression

1111import qualified Text.Parser.Token as Tok

@@ -53,11 +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

56+tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

5757tryFullExpr syn st input =

5858 case runparser (fullExpr syn) st "" input of

59− Success tm -> Just tm

60− _ -> Nothing

59+ Success tm -> Right tm

60+ Failure e -> Left (Msg (show e))

6161

6262{- | Parses an expression

6363@

src/Idris/Parser.hs+1−1

@@ -37,7 +37,7 @@ import Idris.ParseOps

3737import Idris.ParseExpr

3838import Idris.ParseData

3939

40−import Idris.Docstrings

40+import Idris.Docstrings hiding (Unchecked)

4141

4242import Paths_idris

4343

src/Idris/REPL.hs+13−1

@@ -485,7 +485,19 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =

485485 [] -> Left ("Didn't understand name '" ++ s ++ "'")

486486 [n] -> Right $ sUN n

487487 (n:ns) -> Right $ sNS (sUN n) ns

488−

488+runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrString e) =

489+ do ist <- getIState

490+ let out = displayS . renderPretty 1.0 60 $ pprintErr ist e

491+ msg = (IdeSlave.SymbolAtom "ok", IdeSlave.StringAtom $ out "")

492+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

493+runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrPPrint e) =

494+ do ist <- getIState

495+ let (out, spans) =

496+ displaySpans .

497+ renderPretty 0.9 80 .

498+ fmap (fancifyAnnots ist) $ pprintErr ist e

499+ msg = (IdeSlave.SymbolAtom "ok", out, spans)

500+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

489501

490502-- | Show a term for IDESlave with the specified implicitness

491503ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

test/interactive005/input+3

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

1+:consolewidth 80

12the Nat (1 + 2)

23:exec

34:c bytecode hello.bytecode

45:c c hello

56:doc main

67:reload

8+:consolewidth 80

79:load interactive005.idr

810:total main

911:exec

12+:consolewidth 80

1013:t id

1114:set showimplicits

1215:t id

test/interactive005/run+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

2−idris --quiet interactive005.idr < input

2+idris --nocolour --quiet interactive005.idr < input

33rm -f *.ibc

44rm -f hello.bytecode

55rm -f hello