0f98883 · Idris-dev · git.iko.soy

libs/prelude/Prelude/Chars.idr+1−1

compare with master

unifiedsplit

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

1−-- | Functions operating over Char's

2module Prelude.Char

1module Prelude.Char

2+-- Functions operating over Chars

3

4import Builtins

5

libs/prelude/Prelude/Maybe.idr+1−1

@@ -64,7 +64,7 @@ instance (Eq a) => Eq (Maybe a) where

64 (Just _) == Nothing = False

65 (Just a) == (Just b) = a == b

66

67−-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to

67+-- Lift a semigroup into 'Maybe' forming a 'Monoid' according to

68-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be

69-- turned into a monoid simply by adjoining an element i not in S

70-- and defining i+i = i and i+s = s = s+i for all s in S."

src/Idris/ParseData.hs+1−1

@@ -182,7 +182,7 @@ simpleConstructor syn

182 fc <- getFC

183 args <- many (do notEndApp

184 simpleExpr syn)

185− doc <- option "" (docComment '^')

185+ doc <- option "" (try $ docComment '^')

186 return (doc, cn, args, fc, [])

187 <?> "constructor"

188

src/Idris/ParseHelpers.hs+23−6

@@ -78,7 +78,10 @@ isDocCommentMarker _ = False

78 -}

79singleLineComment :: MonadicParsing m => m ()

80singleLineComment = try (string "--" *> eol *> pure ())

81+ <|> try (string "--" *> many simpleWhiteSpace *>

81− <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()

82+ satisfy (not . isDocCommentMarker) *>

83+ many (satisfy (not . isEol)) *>

84+ eol *> pure ())

82 <?> ""

85 <?> ""

83

86

84{- | Consumes a multi-line comment

87{- | Consumes a multi-line comment

@@ -122,12 +125,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

122@

125@

123 -}

126 -}

124docComment :: MonadicParsing m => Char -> m String

127docComment :: MonadicParsing m => Char -> m String

125−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

128+docComment marker | isDocCommentMarker marker = do dc <- docComment' marker

129+ return (T.unpack $ T.strip $ T.pack dc)

126− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

130+ | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"

127 where docComment' :: MonadicParsing m => Char -> m String

131 where docComment' :: MonadicParsing m => Char -> m String

128− docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* eol

132+ docComment' marker = (do string "--"

133+ many (satisfy isSpace)

134+ char marker

135+ res <- many (satisfy (not . isEol))

136+ eol

137+ rest <- many (do string "--"

138+ stuff <- many (satisfy (not . isEol))

139+ eol

140+ return stuff)

141+ someSpace

142+ return (res ++ concat rest))-- ++ concat rest))

143+ <|> (do string "{-"

144+ many (satisfy isSpace)

145+ char marker

129− <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")

146+ (manyTill anyChar (try (string "-}")) <?> "end of comment"))

130− <?> ""

147+ <?> ""

131

148

132-- | Parses some white space

149-- | Parses some white space

133whiteSpace :: MonadicParsing m => m ()

150whiteSpace :: MonadicParsing m => m ()

src/Idris/Parser.hs+2−1

@@ -312,9 +312,10 @@ fnDecl syn = try (do notEndBlock

312fnDecl' :: SyntaxInfo -> IdrisParser PDecl

313fnDecl' syn = checkFixity $

314 do (doc, fc, opts', n, acc) <- try (do

315− doc <- option "" (docComment '|')

316 pushIndent

315 pushIndent

317 ist <- get

316 ist <- get

317+ doc <- option "" (docComment '|')

318+ ist <- get

318 let initOpts = if default_total ist

319 let initOpts = if default_total ist

319 then [TotalFn]

320 then [TotalFn]

320 else []

321 else []