e90316a · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

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

28 documentation lookups, and with semantic highlighting for IDEs.

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

30 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.

31* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

33* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

32 Engine style)

34 Engine style)

33

35

idris.cabal+1−1

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

692 , ansi-terminal < 0.7

693 , ansi-wl-pprint < 0.7

694 , base64-bytestring < 1.1

695− , binary < 0.8

695+ , binary >= 0.7 && < 0.8

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

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

698 , bytestring < 0.11

src/Idris/AbsSyntax.hs+1−1

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

286addCoercion n = do i <- getIState

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

288

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

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

290addDocStr n doc args

291 = do i <- getIState

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

src/Idris/AbsSyntaxTree.hs+16−15

@@ -158,7 +158,7 @@ data IState = IState {

158 idris_flags :: Ctxt [FnOpt],

159 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

160 idris_calledgraph :: Ctxt [Name],

161− idris_docstrings :: Ctxt (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]),

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

162 idris_tyinfodata :: Ctxt TIData,

163 idris_fninfo :: Ctxt FnInfo,

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

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

536-- datatypes and typeclasses.

537data PDecl' t

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

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

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

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

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

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

542 | 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.

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

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

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

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

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

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

548 [t] -- constraints

549 Name

550 [(Name, t)] -- parameters

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

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

552 [PDecl' t] -- declarations

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

554 -- class name, parameters, method declarations

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

599-- | Data declaration

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

601 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

603 }

604 -- ^ Data declaration

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

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

1079unitCon = sUN "MkUnit"

1080

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

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

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

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

1084 "\n\n" ++

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

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

1091

1092eqTy = sUN "="

1093eqCon = sUN "Refl"

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

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

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

1096 "\n\n" ++

1097 "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)]

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

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

1116 where n a = sUN a

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

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

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

1119 "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"),

1120+ reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . 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.")]

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

1122

1123−eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left 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 Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")

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

1125 ]

1126 where n a = sUN a

1127

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

1188 colour ItalicText = IdrisColour Nothing True False False True

1189consoleDecorate ist (AnnTerm _ _) = id

1190consoleDecorate ist (AnnSearchResult _) = id

1191+consoleDecorate ist (AnnErr _) = id

1191

1192

1192isPostulateName :: Name -> IState -> Bool

1193isPostulateName :: Name -> IState -> Bool

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

1194isPostulateName 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

103 | AnnTextFmt TextFormatting

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

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

106+ | AnnErr Err

106

107

107-- | Used for error reflection

108-- | Used for error reflection

108data ErrorReportPart = TextPart String

109data ErrorReportPart = TextPart String

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

117

118

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

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

119-- if they reach the top level.

120-- if they reach the top level.

120−data Err' t

121+data Err' t

121 = Msg String

122 = Msg String

122 | InternalMsg String

123 | InternalMsg String

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

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

src/Idris/Delaborate.hs+6−4

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

9import Idris.AbsSyntax

10import Idris.Core.TT

11import Idris.Core.Evaluate

12−import Idris.Docstrings (overview, renderDocstring)

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

13import Idris.ErrReverse

14

15import Data.List (intersperse, nub)

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

435 _ | otherwise -> annot

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

437 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) []

439 -- TODO make width configurable

440 -- TODO make width configurable

440 -- Issue #1588 on the Issue Tracker

441 -- Issue #1588 on the Issue Tracker

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

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

442− out = displayS . renderPretty 1.0 50 $

443+ out = displayS . renderPretty 1.0 50 $

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

444+ renderDocstring (renderDocTerm (pprintDelab ist)

445+ norm) o

444 return (out "")

446 return (out "")

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

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

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

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

src/Idris/Docs.hs+12−12

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

6import Idris.Delaborate

7import Idris.Core.TT

8import Idris.Core.Evaluate

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

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

10

11import Util.Pretty

12

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

18--

19-- Issue #1573 on the Issue tracker.

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

21−data FunDoc = FD Name (Docstring (Maybe Term))

21+data FunDoc = FD Name (Docstring DocTerm)

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

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

23 PTerm -- function type

24 (Maybe Fixity)

25− deriving Show

26

25

27data Docs = FunDoc FunDoc

26data Docs = FunDoc FunDoc

28 | DataDoc FunDoc -- type constructor docs

27 | DataDoc FunDoc -- type constructor docs

29 [FunDoc] -- data constructor docs

28 [FunDoc] -- data constructor docs

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

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

31 [FunDoc] -- method docs

30 [FunDoc] -- method docs

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

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

33 [PTerm] -- instances

32 [PTerm] -- instances

34 [PTerm] -- superclasses

33 [PTerm] -- superclasses

35− deriving Show

36

34

35+showDoc ist d

37−showDoc ist d | nullDocstring d = empty

36+ | nullDocstring d = empty

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

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

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

39

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

41pprintFD ist (FD n doc args ty f)

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

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

44 , 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 <$>

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

47 let argshow = showArgs args [] in

48 if not (null argshow)

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

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

85 if nullDocstring doc

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

88 <> line <$>

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

90 <> line <$>

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

187 funName (UN n) = str n

188 funName (NS n _) = funName n

189

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

191getPArgNames (PPi plicity name ty body) ds =

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

193getPArgNames _ _ = []

src/Idris/Docstrings.hs+79−39

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

1{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

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

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

3

4-- | Wrapper around Markdown library

5module Idris.Docstrings (

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

7− overview, containsText, renderHtml, annotCode

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

8 ) where

9

10import qualified Cheapskate as C

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

13

14import Util.Pretty

15

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

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

17

18import qualified Data.Text as T

19import qualified Data.Foldable as F

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

25

26import Text.Blaze.Html (Html)

27

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+

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

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

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

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

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

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

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

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

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

59

75

60

76

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+

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

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

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

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

63parseDocstring = toDocstring . C.markdown options

110parseDocstring = toDocstring . C.markdown options

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

94 }

141 }

95

142

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

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

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

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

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

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

99

146

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

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

101-- argument docstring, for use in summaries.

148-- argument docstring, for use in summaries.

102overview :: Docstring a -> Docstring a

149overview :: Docstring a -> Docstring a

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

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

104

151

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

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

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

153+ -> Blocks a -> Doc OutputAnnotation

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

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

108− fmap (renderBlock pp norm) blocks

155+ fmap (renderBlock pp) blocks

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

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

110 | otherwise = empty

157 | otherwise = empty

111

158

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

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

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

160+ -> Block a -> Doc OutputAnnotation

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

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

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

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

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

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

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

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

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

165+renderBlock pp (CodeBlock attr src tm) = indent 4 $ pp tm (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

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

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

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

127−

168+

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

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

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

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

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

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

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

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

132 vsep $

173 vsep $

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

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

135 where punc = case nw of

176 where punc = case nw of

136 CT.PeriodFollowing -> char '.'

177 CT.PeriodFollowing -> char '.'

137 CT.ParenFollowing -> char '('

178 CT.ParenFollowing -> char '('

138

179

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

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

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

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

141

182

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

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

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

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

144renderInline pp Space = softline

185renderInline pp Space = softline

145renderInline pp SoftBreak = softline

186renderInline pp SoftBreak = softline

146renderInline pp LineBreak = line

187renderInline pp LineBreak = line

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

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

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

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

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

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

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

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

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

152 parens (text $ T.unpack url)

192 parens (text $ T.unpack url)

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

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

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

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

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

194

234

195

235

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

236+renderHtml :: Docstring DocTerm -> Html

197renderHtml = renderDoc . fromDocstring

237renderHtml = renderDoc . fromDocstring

198 where

238 where

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

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

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

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

201

241

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

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

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

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

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

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

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

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

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

208 fromBlock (HtmlBlock src) = CT.HtmlBlock src

248 fromBlock (HtmlBlock src) = CT.HtmlBlock src

209 fromBlock HRule = CT.HRule

249 fromBlock HRule = CT.HRule

210

250

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

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

212 fromInline (Str t) = CT.Str t

252 fromInline (Str t) = CT.Str t

213 fromInline Space = CT.Space

253 fromInline Space = CT.Space

214 fromInline SoftBreak = CT.SoftBreak

254 fromInline SoftBreak = CT.SoftBreak

src/Idris/Elab/Class.hs+2−2

@@ -52,9 +52,9 @@ import Util.Pretty(pretty, text)

52

53data MArgTy = IA | EA | CA deriving Show

54

55−elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

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

56 FC -> [PTerm] ->

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

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [PDecl] -> Idris ()

58elabClass info syn_in doc fc constraints tn ps pDocs ds

59 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

60 let tty = pibind ps PType

src/Idris/Elab/Clause.hs+1−1

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

30import Idris.Core.Typecheck

31import Idris.Core.CaseTree

32

33−import Idris.Docstrings

33+import Idris.Docstrings hiding (Unchecked)

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

35

36import Prelude hiding (id, (.))

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

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

50

51import Util.Pretty(pretty, text)

52

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

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

55 = do let codata = Codata `elem` opts

56 iLOG (show (fc, doc))

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

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

79 ttag <- getName

80 i <- getIState

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

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

82 let params = findParams (map snd cons)

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

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

206

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

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

210 Idris (Name, Type)

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

212 = do checkUndefined fc n

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

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

280-- rename to caseFun to match updated intend

281elabCaseFun :: 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])] ->

283 ElabInfo -> EliminatorState ()

284elabCaseFun ind paramPos n ty cons info = do

285 elimLog $ "Elaborating case function"

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

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

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

300 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

302 let clauseConsElimArgs = map getPiName consTerms

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

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

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

448 splitArgPms _ = ([],[])

449

450

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

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

453 i <- State.lift getIState

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

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

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

464 _ -> return implargs

465

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

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

468 let cons' = replaceParams paramPos generalParameters ty

469 let (args, resTy) = splitPi cons'

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

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

500 convertImplPi _ = Nothing

501

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

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

504 let cons' = replaceParams paramPos generalParameters ty

505 let (args, resTy) = splitPi cons'

src/Idris/Elab/Provider.hs+1−1

@@ -98,7 +98,7 @@ elabProvider info syn fc what n

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

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

102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103 | otherwise ->

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

50

51import Util.Pretty(pretty, text)

52

53−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> FC -> Name ->

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

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

54+ PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Name -> PTerm -> Idris ()

55elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

56 = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

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

114 param_pos i ns t = []

115

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

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

119elabType = elabType' False

120

121elabType' :: 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))] ->

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

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

125 n = liftname info n_in in -}

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

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

208 tyIsHandler _ = False

209

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

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

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

212elabPostulate info syn doc fc opts n ty = do

213 elabType info syn doc [] fc opts n ty

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

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

1{-# LANGUAGE PatternGuards #-}

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

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

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

3

4

4import Idris.AbsSyntax

5import Idris.AbsSyntax

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

22

23

23import Idris.Core.TT

24import Idris.Core.TT

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

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

25−import Idris.Core.Evaluate

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

26import Idris.Core.Execute

27import Idris.Core.Execute

27import Idris.Core.Typecheck

28import Idris.Core.Typecheck

28import Idris.Core.CaseTree

29import Idris.Core.CaseTree

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

88

89

90

91

91−elabDocTerms :: ElabInfo -> Docstring (Maybe PTerm) -> Idris (Docstring (Maybe Term))

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

92−elabDocTerms info str = Traversable.mapM decorate str

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

94+ return $ checkDocstring mkDocTerm typechecked

93− where decorate Nothing = return Nothing

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

94− decorate (Just pt) = fmap (fmap fst) (tryElabVal info ERHS pt)

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

97+

95− tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Maybe (Term, Type))

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

96 tryElabVal info aspat tm_in

99 tryElabVal info aspat tm_in

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

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

98− (const $ return Nothing)

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

38import Idris.Core.Typecheck

39import Idris.Core.CaseTree

40

41−import Idris.Docstrings

41+import Idris.Docstrings hiding (Unchecked)

42

43import Prelude hiding (id, (.))

44import Control.Category

src/Idris/IBC.hs+17−3

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

32import Util.Zlib (decompressEither)

33

34ibcVersion :: Word8

35−ibcVersion = 83

35+ibcVersion = 84

36

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

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

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

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

63 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)]))],

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

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

67 ibc_coercions :: [Name],

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

459 update (Proj t i) = Proj (update t) i

460 update t = t

461

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

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

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

464

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

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

538 x4 <- get

539 return (CT.Options x1 x2 x3 x4)

540

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+

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

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

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

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

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

557 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+

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

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

2

4

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

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

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

151 EQ -> "isomorphic"

153 EQ -> "isomorphic"

152 LT -> "more general than searched type"

154 LT -> "more general than searched type"

153 GT -> "more specific than searched type"

155 GT -> "more specific than searched type"

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

154

157

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

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

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

159encodeTerm 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

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

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

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

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

161

164

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+

162instance SExpable FC where

171instance SExpable FC where

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

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

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

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

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

219 | TermShowImplicits [(Name, Bool)] Term

228 | TermShowImplicits [(Name, Bool)] Term

220 | TermNoImplicits [(Name, Bool)] Term

229 | TermNoImplicits [(Name, Bool)] Term

221 | PrintDef String

230 | PrintDef String

231+ | ErrString Err

232+ | ErrPPrint Err

222

233

223sexpToCommand :: SExp -> Maybe IdeSlaveCommand

234sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

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

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

263 Just (TermNoImplicits bnd tm)

274 Just (TermNoImplicits bnd tm)

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

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

265sexpToCommand _ = Nothing

278sexpToCommand _ = Nothing

266

279

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

280parseMessage :: 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 #-}

2

3module Idris.Output where

4

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

177

178

179prettyDocumentedIst :: IState

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

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

181 -> Doc OutputAnnotation

182prettyDocumentedIst ist (name, ty, docs) =

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

185 where ppTm = pprintDelab ist

186+ norm = normaliseAll (tt_ctxt ist) []

186

187

188

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

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

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

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

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

221 decorate HTMLOutput (AnnTerm _ _) = id

222 decorate HTMLOutput (AnnTerm _ _) = id

222 decorate HTMLOutput (AnnSearchResult _) = id

223 decorate HTMLOutput (AnnSearchResult _) = id

224+ decorate HTMLOutput (AnnErr _) = id

223

225

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

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

225 latex "IdrisType"

227 latex "IdrisType"

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

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

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

243 decorate LaTeXOutput (AnnTerm _ _) = id

245 decorate LaTeXOutput (AnnTerm _ _) = id

244 decorate LaTeXOutput (AnnSearchResult _) = id

246 decorate LaTeXOutput (AnnSearchResult _) = id

247+ decorate LaTeXOutput (AnnErr _) = id

245

248

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

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

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

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

src/Idris/ParseData.hs+3−3

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

4import Prelude hiding (pi)

5

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

8import Text.Parser.LookAhead

9import Text.Parser.Expression

10import qualified Text.Parser.Token as Tok

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

172{- | Parses a type constructor declaration

173 Constructor ::= DocComment? FnName TypeSig;

174-}

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

176constructor syn

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

178 cn_in <- fnName; fc <- getFC

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

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

192 SimpleConstructor ::= FnName SimpleExpr* DocComment?

193-}

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

195simpleConstructor syn

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

197 ist <- get

src/Idris/ParseExpr.hs+4−4

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

5import Prelude hiding (pi)

6

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

9import Text.Parser.LookAhead

10import Text.Parser.Expression

11import qualified Text.Parser.Token as Tok

@@ -53,11 +53,11 @@ fullExpr syn = do x <- expr syn

53 i <- get

54 return $ debindApp syn (desugar syn i x)

55

56−tryFullExpr :: SyntaxInfo -> IState -> String -> Maybe PTerm

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

57tryFullExpr syn st input =

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

59− Success tm -> Just tm

59+ Success tm -> Right tm

60− _ -> Nothing

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

61

62{- | Parses an expression

63@

src/Idris/Parser.hs+1−1

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

37import Idris.ParseExpr

38import Idris.ParseData

39

40−import Idris.Docstrings

40+import Idris.Docstrings hiding (Unchecked)

41

42import Paths_idris

43

src/Idris/REPL.hs+13−1

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

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

486 [n] -> Right $ sUN n

487 (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

489

501

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

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

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

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

test/interactive005/input+3

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

1+:consolewidth 80

1the Nat (1 + 2)

2the Nat (1 + 2)

2:exec

3:exec

3:c bytecode hello.bytecode

4:c bytecode hello.bytecode

4:c c hello

5:c c hello

5:doc main

6:doc main

6:reload

7:reload

8+:consolewidth 80

7:load interactive005.idr

9:load interactive005.idr

8:total main

10:total main

9:exec

11:exec

12+:consolewidth 80

10:t id

13:t id

11:set showimplicits

14:set showimplicits

12:t id

15:t id

test/interactive005/run+1−1

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

1#!/usr/bin/env bash

2−idris --quiet interactive005.idr < input

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

3rm -f *.ibc

4rm -f hello.bytecode

5rm -f hello