1ccd94a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Syntax for documentation comments and :doc REPL command

1ccd94aEdwin Brady14 years ago

src/Core/CoreParser.hs+367−13

compare with master

unifiedsplit

@@ -8,10 +8,15 @@ import Core.TT

8import Text.ParserCombinators.Parsec

9import Text.ParserCombinators.Parsec.Expr

10import Text.ParserCombinators.Parsec.Language

11+import Text.ParserCombinators.Parsec.Prim

12+import Text.ParserCombinators.Parsec.Char

13+import Text.ParserCombinators.Parsec.Combinator

11import qualified Text.ParserCombinators.Parsec.Token as PTok

14import qualified Text.ParserCombinators.Parsec.Token as PTok

13import Control.Monad.State

16import Control.Monad.State

17+import Control.Monad.Identity

14import Data.Char

18import Data.Char

19+import Data.List

15import Debug.Trace

20import Debug.Trace

17type TokenParser a = PTok.TokenParser a

22type TokenParser a = PTok.TokenParser a

@@ -38,21 +43,22 @@ iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

38-- <|> letter

43-- <|> letter

40idrisLexer :: TokenParser a

45idrisLexer :: TokenParser a

41−idrisLexer = (PTok.makeTokenParser idrisDef) { PTok.whiteSpace = lexWS }

46+idrisLexer = idrisMakeTokenParser idrisDef

43lexer = idrisLexer

48lexer = idrisLexer

45-- Taken from Parsec source code

50-- Taken from Parsec source code

51+lexWS = do i <- getInput

46−lexWS = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")

52+ skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")

47 where

53 where

49 simpleSpace = skipMany1 (satisfy isSpace)

55 simpleSpace = skipMany1 (satisfy isSpace)

50− oneLineComment = do try (string ("--"))

56+ oneLineComment = do try (do string ("--")

51− satisfy (/= '|')

57+ satisfy (\x -> x /= '|' && x /= '^'))

52 skipMany (satisfy (/= '\n'))

58 skipMany (satisfy (/= '\n'))

53 return ()

59 return ()

54− multiLineComment = do try (string "{-")

60+ multiLineComment = do try (do string "{-"

55− satisfy (/= '|')

61+ satisfy (\x -> x /= '|' && x /= '^'))

56 inCommentMulti

62 inCommentMulti

58 inCommentMulti

64 inCommentMulti

@@ -75,6 +81,7 @@ identifier= PTok.identifier lexer

75reserved = PTok.reserved lexer

81reserved = PTok.reserved lexer

76operator = PTok.operator lexer

82operator = PTok.operator lexer

77reservedOp= PTok.reservedOp lexer

83reservedOp= PTok.reservedOp lexer

84+strlit = PTok.stringLiteral lexer

78lchar = lexeme.char

85lchar = lexeme.char

80type CParser a = GenParser Char a

87type CParser a = GenParser Char a

@@ -124,13 +131,23 @@ mkName (n, ns) = NS (UN n) (reverse (parseNS ns))

124 (x, '.':y) -> x : parseNS y

131 (x, '.':y) -> x : parseNS y

125

132

126pDocComment :: Char -> CParser a String

133pDocComment :: Char -> CParser a String

127−pDocComment c

134+pDocComment c

128− = do string "--"

135+ = try (do string ("--" ++ [c])

129− char c

130− i <- getInput

136+ i <- getInput

131− let (doc, rest) = span (/='\n') i

137+ let (doc, rest) = span (/='\n') i

138+ setInput rest

139+ whiteSpace

140+ return doc)

141+ <|> try (do string ("{-" ++ [c])

142+ i <- getInput

143+ -- read to '-}'

144+ let (doc, rest) = spanComment "" i

132− setInput rest

145+ setInput rest

146+ whiteSpace

133− return doc

147+ return doc)

148+ where spanComment acc ('-':'}':xs) = (reverse acc, xs)

149+ spanComment acc (x:xs) = spanComment (x : acc) xs

150+ spanComment acc [] = (acc, [])

134

151

135pDef :: CParser a (Name, RDef)

152pDef :: CParser a (Name, RDef)

136pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

153pDef = try (do x <- iName []; lchar ':'; ty <- pTerm

@@ -208,3 +225,340 @@ pConstructor = do lchar '|'

208 c <- iName []; lchar ':'; ty <- pTerm

225 c <- iName []; lchar ':'; ty <- pTerm

209 return (c, ty)

226 return (c, ty)

210

227

228+------ borrowed from Parsec

229+-- (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

230+

231+idrisMakeTokenParser languageDef

232+ = PTok.TokenParser{

233+ PTok.identifier = identifier

234+ , PTok.reserved = reserved

235+ , PTok.operator = operator

236+ , PTok.reservedOp = reservedOp

237+

238+ , PTok.charLiteral = charLiteral

239+ , PTok.stringLiteral = stringLiteral

240+ , PTok.natural = natural

241+ , PTok.integer = integer

242+ , PTok.float = float

243+ , PTok.naturalOrFloat = naturalOrFloat

244+ , PTok.decimal = decimal

245+ , PTok.hexadecimal = hexadecimal

246+ , PTok.octal = octal

247+

248+ , PTok.symbol = symbol

249+ , PTok.lexeme = lexeme

250+ , PTok.whiteSpace = lexWS

251+

252+ , PTok.parens = parens

253+ , PTok.braces = braces

254+ , PTok.angles = angles

255+ , PTok.brackets = brackets

256+ , PTok.squares = brackets

257+ , PTok.semi = semi

258+ , PTok.comma = comma

259+ , PTok.colon = colon

260+ , PTok.dot = dot

261+ , PTok.semiSep = semiSep

262+ , PTok.semiSep1 = semiSep1

263+ , PTok.commaSep = commaSep

264+ , PTok.commaSep1 = commaSep1

265+ }

266+ where

267+

268+ -----------------------------------------------------------

269+ -- Bracketing

270+ -----------------------------------------------------------

271+ parens p = between (symbol "(") (symbol ")") p

272+ braces p = between (symbol "{") (symbol "}") p

273+ angles p = between (symbol "<") (symbol ">") p

274+ brackets p = between (symbol "[") (symbol "]") p

275+

276+ semi = symbol ";"

277+ comma = symbol ","

278+ dot = symbol "."

279+ colon = symbol ":"

280+

281+ commaSep p = sepBy p comma

282+ semiSep p = sepBy p semi

283+

284+ commaSep1 p = sepBy1 p comma

285+ semiSep1 p = sepBy1 p semi

286+

287+

288+ -----------------------------------------------------------

289+ -- Chars & Strings

290+ -----------------------------------------------------------

291+ charLiteral = lexeme (between (char '\'')

292+ (char '\'' <?> "end of character")

293+ characterChar )

294+ <?> "character"

295+

296+ characterChar = charLetter <|> charEscape

297+ <?> "literal character"

298+

299+ charEscape = do{ char '\\'; escapeCode }

300+ charLetter = satisfy (\c -> (c /= '\'') && (c /= '\\') && (c > '\026'))

301+

302+

303+

304+ stringLiteral = lexeme (

305+ do{ str <- between (char '"')

306+ (char '"' <?> "end of string")

307+ (many stringChar)

308+ ; return (foldr (maybe id (:)) "" str)

309+ }

310+ <?> "literal string")

311+

312+ stringChar = do{ c <- stringLetter; return (Just c) }

313+ <|> stringEscape

314+ <?> "string character"

315+

316+ stringLetter = satisfy (\c -> (c /= '"') && (c /= '\\') && (c > '\026'))

317+

318+ stringEscape = do{ char '\\'

319+ ; do{ escapeGap ; return Nothing }

320+ <|> do{ escapeEmpty; return Nothing }

321+ <|> do{ esc <- escapeCode; return (Just esc) }

322+ }

323+

324+ escapeEmpty = char '&'

325+ escapeGap = do{ many1 space

326+ ; char '\\' <?> "end of string gap"

327+ }

328+

329+

330+

331+ -- escape codes

332+ escapeCode = charEsc <|> charNum <|> charAscii <|> charControl

333+ <?> "escape code"

334+

335+ charControl = do{ char '^'

336+ ; code <- upper

337+ ; return (toEnum (fromEnum code - fromEnum 'A'))

338+ }

339+

340+ charNum = do{ code <- decimal

341+ <|> do{ char 'o'; number 8 octDigit }

342+ <|> do{ char 'x'; number 16 hexDigit }

343+ ; return (toEnum (fromInteger code))

344+ }

345+

346+ charEsc = choice (map parseEsc escMap)

347+ where

348+ parseEsc (c,code) = do{ char c; return code }

349+

350+ charAscii = choice (map parseAscii asciiMap)

351+ where

352+ parseAscii (asc,code) = try (do{ string asc; return code })

353+

354+

355+ -- escape code tables

356+ escMap = zip ("abfnrtv\\\"\'") ("\a\b\f\n\r\t\v\\\"\'")

357+ asciiMap = zip (ascii3codes ++ ascii2codes) (ascii3 ++ ascii2)

358+

359+ ascii2codes = ["BS","HT","LF","VT","FF","CR","SO","SI","EM",

360+ "FS","GS","RS","US","SP"]

361+ ascii3codes = ["NUL","SOH","STX","ETX","EOT","ENQ","ACK","BEL",

362+ "DLE","DC1","DC2","DC3","DC4","NAK","SYN","ETB",

363+ "CAN","SUB","ESC","DEL"]

364+

365+ ascii2 = ['\BS','\HT','\LF','\VT','\FF','\CR','\SO','\SI',

366+ '\EM','\FS','\GS','\RS','\US','\SP']

367+ ascii3 = ['\NUL','\SOH','\STX','\ETX','\EOT','\ENQ','\ACK',

368+ '\BEL','\DLE','\DC1','\DC2','\DC3','\DC4','\NAK',

369+ '\SYN','\ETB','\CAN','\SUB','\ESC','\DEL']

370+

371+

372+ -----------------------------------------------------------

373+ -- Numbers

374+ -----------------------------------------------------------

375+ naturalOrFloat = lexeme (natFloat) <?> "number"

376+

377+ float = lexeme floating <?> "float"

378+ integer = lexeme int <?> "integer"

379+ natural = lexeme nat <?> "natural"

380+

381+

382+ -- floats

383+ floating = do{ n <- decimal

384+ ; fractExponent n

385+ }

386+

387+

388+ natFloat = do{ char '0'

389+ ; zeroNumFloat

390+ }

391+ <|> decimalFloat

392+

393+ zeroNumFloat = do{ n <- hexadecimal <|> octal

394+ ; return (Left n)

395+ }

396+ <|> decimalFloat

397+ <|> fractFloat 0

398+ <|> return (Left 0)

399+

400+ decimalFloat = do{ n <- decimal

401+ ; option (Left n)

402+ (fractFloat n)

403+ }

404+

405+ fractFloat n = do{ f <- fractExponent n

406+ ; return (Right f)

407+ }

408+

409+ fractExponent n = do{ fract <- fraction

410+ ; expo <- option 1.0 exponent'

411+ ; return ((fromInteger n + fract)*expo)

412+ }

413+ <|>

414+ do{ expo <- exponent'

415+ ; return ((fromInteger n)*expo)

416+ }

417+

418+ fraction = do{ char '.'

419+ ; digits <- many1 digit <?> "fraction"

420+ ; return (foldr op 0.0 digits)

421+ }

422+ <?> "fraction"

423+ where

424+ op d f = (f + fromIntegral (digitToInt d))/10.0

425+

426+ exponent' = do{ oneOf "eE"

427+ ; f <- sign

428+ ; e <- decimal <?> "exponent"

429+ ; return (power (f e))

430+ }

431+ <?> "exponent"

432+ where

433+ power e | e < 0 = 1.0/power(-e)

434+ | otherwise = fromInteger (10^e)

435+

436+

437+ -- integers and naturals

438+ int = do{ f <- lexeme sign

439+ ; n <- nat

440+ ; return (f n)

441+ }

442+

443+ sign = (char '-' >> return negate)

444+ <|> (char '+' >> return id)

445+ <|> return id

446+

447+ nat = zeroNumber <|> decimal

448+

449+ zeroNumber = do{ char '0'

450+ ; hexadecimal <|> octal <|> decimal <|> return 0

451+ }

452+ <?> ""

453+

454+ decimal = number 10 digit

455+ hexadecimal = do{ oneOf "xX"; number 16 hexDigit }

456+ octal = do{ oneOf "oO"; number 8 octDigit }

457+

458+ number base baseDigit

459+ = do{ digits <- many1 baseDigit

460+ ; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits

461+ ; seq n (return n)

462+ }

463+

464+ -----------------------------------------------------------

465+ -- Operators & reserved ops

466+ -----------------------------------------------------------

467+ reservedOp name =

468+ lexeme $ try $

469+ do{ string name

470+ ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)

471+ }

472+

473+ operator =

474+ lexeme $ try $

475+ do{ name <- oper

476+ ; if (isReservedOp name)

477+ then unexpected ("reserved operator " ++ show name)

478+ else return name

479+ }

480+

481+ oper =

482+ do{ c <- (opStart languageDef)

483+ ; cs <- many (opLetter languageDef)

484+ ; return (c:cs)

485+ }

486+ <?> "operator"

487+

488+ isReservedOp name =

489+ isReserved (sort (reservedOpNames languageDef)) name

490+

491+

492+ -----------------------------------------------------------

493+ -- Identifiers & Reserved words

494+ -----------------------------------------------------------

495+ reserved name =

496+ lexeme $ try $

497+ do{ caseString name

498+ ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)

499+ }

500+

501+ caseString name

502+ | caseSensitive languageDef = string name

503+ | otherwise = do{ walk name; return name }

504+ where

505+ walk [] = return ()

506+ walk (c:cs) = do{ caseChar c <?> msg; walk cs }

507+

508+ caseChar c | isAlpha c = char (toLower c) <|> char (toUpper c)

509+ | otherwise = char c

510+

511+ msg = show name

512+

513+

514+ identifier =

515+ lexeme $ try $

516+ do{ name <- ident

517+ ; if (isReservedName name)

518+ then unexpected ("reserved word " ++ show name)

519+ else return name

520+ }

521+

522+

523+ ident

524+ = do{ c <- identStart languageDef

525+ ; cs <- many (identLetter languageDef)

526+ ; return (c:cs)

527+ }

528+ <?> "identifier"

529+

530+ isReservedName name

531+ = isReserved theReservedNames caseName

532+ where

533+ caseName | caseSensitive languageDef = name

534+ | otherwise = map toLower name

535+

536+

537+ isReserved names name

538+ = scan names

539+ where

540+ scan [] = False

541+ scan (r:rs) = case (compare r name) of

542+ LT -> scan rs

543+ EQ -> True

544+ GT -> False

545+

546+ theReservedNames

547+ | caseSensitive languageDef = sortedNames

548+ | otherwise = map (map toLower) sortedNames

549+ where

550+ sortedNames = sort (reservedNames languageDef)

551+

552+

553+

554+ -----------------------------------------------------------

555+ -- White space & symbols

556+ -----------------------------------------------------------

557+ symbol name

558+ = lexeme (string name)

559+

560+ lexeme p

561+ = do{ x <- p; whiteSpace; return x }

562+

563+ --whiteSpace

564+ whiteSpace = lexWS

src/Idris/AbsSyntaxTree.hs+1

@@ -143,6 +143,7 @@ data Command = Quit

143 | Help

144 | Eval PTerm

145 | Check PTerm

146+ | DocStr Name

146 | TotCheck Name

147 | TotCheck Name

147 | Reload

148 | Reload

148 | Load FilePath

149 | Load FilePath

src/Idris/ElabDecls.hs+6

@@ -72,6 +72,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

72 addIBC (IBCDef n)

73 addDeferred ds

74 setFlags n opts'

75+ addDocStr n doc

76+ addIBC (IBCDoc n)

75 addIBC (IBCFlags n opts')

77 addIBC (IBCFlags n opts')

76 when corec $ do setAccessibility n Frozen

78 when corec $ do setAccessibility n Frozen

77 addIBC (IBCAccess n Frozen)

79 addIBC (IBCAccess n Frozen)

@@ -116,6 +118,8 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

116 (idris_datatypes i) })

118 (idris_datatypes i) })

117 addIBC (IBCDef n)

119 addIBC (IBCDef n)

118 addIBC (IBCData n)

120 addIBC (IBCData n)

121+ addDocStr n doc

122+ addIBC (IBCDoc n)

119 collapseCons n cons

123 collapseCons n cons

120 updateContext (addDatatype (Data n ttag cty cons))

124 updateContext (addDatatype (Data n ttag cty cons))

121 mapM_ (checkPositive n) cons

125 mapM_ (checkPositive n) cons

@@ -250,6 +254,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)

250 tyIs cty'

254 tyIs cty'

251 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

255 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

252 addIBC (IBCDef n)

256 addIBC (IBCDef n)

257+ addDocStr n doc

258+ addIBC (IBCDoc n)

253 forceArgs n cty'

259 forceArgs n cty'

254 return (n, cty')

260 return (n, cty')

255 where

261 where

src/Idris/Parser.hs+24−14

@@ -423,7 +423,10 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

423 return (Symbol sym)

424

425pFunDecl' :: SyntaxInfo -> IParser PDecl

426+pFunDecl' syn = try (do doc <- option "" (pDocComment '|')

427+ -- trace ("Doc: " ++ show doc) $

428+-- let doc = ""

426−pFunDecl' syn = try (do pushIndent

429+ pushIndent

427 ist <- getState

430 ist <- getState

428 let initOpts = if default_total ist

431 let initOpts = if default_total ist

429 then [TotalFn]

432 then [TotalFn]

@@ -438,7 +441,7 @@ pFunDecl' syn = try (do pushIndent

438 pTerminator

441 pTerminator

439-- ty' <- implicit syn n ty

442-- ty' <- implicit syn n ty

440 addAcc n acc

443 addAcc n acc

441− return (PTy "" syn fc opts' n ty))

444+ return (PTy doc syn fc opts' n ty))

442 <|> try (pPattern syn)

445 <|> try (pPattern syn)

443 <|> try (pCAF syn)

446 <|> try (pCAF syn)

444

447

@@ -503,7 +506,8 @@ fixity = try (do reserved "infixl"; return Infixl)

503--------- Type classes ---------

506--------- Type classes ---------

504

507

505pClass :: SyntaxInfo -> IParser [PDecl]

508pClass :: SyntaxInfo -> IParser [PDecl]

509+pClass syn = do doc <- option "" (pDocComment '|')

506−pClass syn = do acc <- pAccessibility

510+ acc <- pAccessibility

507 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName

511 reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName

508 let n = expandNS syn n_in

512 let n = expandNS syn n_in

509 cs <- many1 carg

513 cs <- many1 carg

@@ -512,7 +516,7 @@ pClass syn = do acc <- pAccessibility

512 closeBlock

516 closeBlock

513 let allDs = concat ds

517 let allDs = concat ds

514 accData acc n (concatMap declared allDs)

518 accData acc n (concatMap declared allDs)

515− return [PClass "" syn fc cons n cs allDs]

519+ return [PClass doc syn fc cons n cs allDs]

516 where

520 where

517 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

521 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

518 return (i, ty)

522 return (i, ty)

@@ -905,9 +909,10 @@ pPi syn =

905 try (do lazy <- option False (do lchar '|'; return True)

909 try (do lazy <- option False (do lchar '|'; return True)

906 st <- pStatic

910 st <- pStatic

907 lchar '('; xt <- tyDeclList syn; lchar ')'

911 lchar '('; xt <- tyDeclList syn; lchar ')'

912+ doc <- option "" (pDocComment '^')

908 symbol "->"

913 symbol "->"

909 sc <- pExpr syn

914 sc <- pExpr syn

910− return (bindList (PPi (Exp lazy st "")) xt sc))

915+ return (bindList (PPi (Exp lazy st doc)) xt sc))

911 <|> try (if implicitAllowed syn

916 <|> try (if implicitAllowed syn

912 then do lazy <- option False (do lchar '|'

917 then do lazy <- option False (do lchar '|'

913 return True)

918 return True)

@@ -1074,6 +1079,7 @@ toTable fs = map (map toBin)

1074

1079

1075binary name f = Infix (do reservedOp name

1080binary name f = Infix (do reservedOp name

1076 fc <- pfc;

1081 fc <- pfc;

1082+ doc <- option "" (pDocComment '^')

1077 return (f fc))

1083 return (f fc))

1078prefix name f = Prefix (do reservedOp name

1084prefix name f = Prefix (do reservedOp name

1079 fc <- pfc;

1085 fc <- pfc;

@@ -1124,13 +1130,14 @@ pDataI = do reserved "data"; return False

1124 <|> do reserved "codata"; return True

1130 <|> do reserved "codata"; return True

1125

1131

1126pData :: SyntaxInfo -> IParser PDecl

1132pData :: SyntaxInfo -> IParser PDecl

1133+pData syn = try (do doc <- option "" (pDocComment '|')

1127−pData syn = try (do acc <- pAccessibility

1134+ acc <- pAccessibility

1128 co <- pDataI

1135 co <- pDataI

1129 fc <- pfc

1136 fc <- pfc

1130 tyn_in <- pfName

1137 tyn_in <- pfName

1131 ty <- pTSig (impOK syn)

1138 ty <- pTSig (impOK syn)

1132 let tyn = expandNS syn tyn_in

1139 let tyn = expandNS syn tyn_in

1133− option (PData "" syn fc co (PLaterdecl tyn ty)) (do

1140+ option (PData doc syn fc co (PLaterdecl tyn ty)) (do

1134 reserved "where"

1141 reserved "where"

1135 openBlock

1142 openBlock

1136 pushIndent

1143 pushIndent

@@ -1141,8 +1148,9 @@ pData syn = try (do acc <- pAccessibility

1141 popIndent

1148 popIndent

1142 closeBlock

1149 closeBlock

1143 accData acc tyn (map (\ (_, n, _, _) -> n) cons)

1150 accData acc tyn (map (\ (_, n, _, _) -> n) cons)

1144− return $ PData "" syn fc co (PDatadecl tyn ty cons)))

1151+ return $ PData doc syn fc co (PDatadecl tyn ty cons)))

1152+ <|> try (do doc <- option "" (pDocComment '|')

1145− <|> try (do pushIndent

1153+ pushIndent

1146 acc <- pAccessibility

1154 acc <- pAccessibility

1147 co <- pDataI

1155 co <- pDataI

1148 fc <- pfc

1156 fc <- pfc

@@ -1150,7 +1158,7 @@ pData syn = try (do acc <- pAccessibility

1150 args <- many pName

1158 args <- many pName

1151 let ty = bindArgs (map (const PSet) args) PSet

1159 let ty = bindArgs (map (const PSet) args) PSet

1152 let tyn = expandNS syn tyn_in

1160 let tyn = expandNS syn tyn_in

1153− option (PData "" syn fc co (PLaterdecl tyn ty)) (do

1161+ option (PData doc syn fc co (PLaterdecl tyn ty)) (do

1154 lchar '='

1162 lchar '='

1155 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1163 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1156 pTerminator

1164 pTerminator

@@ -1159,7 +1167,7 @@ pData syn = try (do acc <- pAccessibility

1159 do let cty = bindArgs cargs conty

1167 do let cty = bindArgs cargs conty

1160 return (doc, x, cty, cfc)) cons

1168 return (doc, x, cty, cfc)) cons

1161 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

1169 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

1162− return $ PData "" syn fc co (PDatadecl tyn ty cons')))

1170+ return $ PData doc syn fc co (PDatadecl tyn ty cons')))

1163 where

1171 where

1164 mkPApp fc t [] = t

1172 mkPApp fc t [] = t

1165 mkPApp fc t xs = PApp fc t (map pexp xs)

1173 mkPApp fc t xs = PApp fc t (map pexp xs)

@@ -1169,11 +1177,12 @@ bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

1169

1177

1170pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)

1178pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)

1171pConstructor syn

1179pConstructor syn

1180+ = do doc <- option "" (pDocComment '|')

1172− = do cn_in <- pfName; fc <- pfc

1181+ cn_in <- pfName; fc <- pfc

1173 let cn = expandNS syn cn_in

1182 let cn = expandNS syn cn_in

1174 ty <- pTSig (impOK syn)

1183 ty <- pTSig (impOK syn)

1175-- ty' <- implicit syn cn ty

1184-- ty' <- implicit syn cn ty

1176− return ("", cn, ty, fc)

1185+ return (doc, cn, ty, fc)

1177

1186

1178

1187

1179pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)

1188pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)

@@ -1183,7 +1192,8 @@ pSimpleCon syn

1183 fc <- pfc

1192 fc <- pfc

1184 args <- many (do notEndApp

1193 args <- many (do notEndApp

1185 pSimpleExpr syn)

1194 pSimpleExpr syn)

1195+ doc <- option "" (pDocComment '^')

1186− return ("", cn, args, fc)

1196+ return (doc, cn, args, fc)

1187

1197

1188--------- DSL syntax overloading ---------

1198--------- DSL syntax overloading ---------

1189

1199

src/Idris/REPL.hs+6

@@ -196,6 +196,12 @@ process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

196 let ty' = normaliseC ctxt [] ty

197 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

198 showImp imp (delab ist ty))

199+

200+process fn (DocStr n) = do i <- get

201+ case lookupCtxtName Nothing n (idris_docstrings i) of

202+ [] -> iputStrLn "No documentation"

203+ ns -> mapM_ showDoc ns

204+ where showDoc (n, d) = iputStrLn $ show n ++ " : " ++ d

199process fn Universes = do i <- get

205process fn Universes = do i <- get

200 let cs = idris_constraints i

206 let cs = idris_constraints i

201-- iputStrLn $ showSep "\n" (map show cs)

207-- iputStrLn $ showSep "\n" (map show cs)

src/Idris/REPLParser.hs+1

@@ -43,6 +43,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

43 <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

44 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

45 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

46+ <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))

46 <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))

47 <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))

47 <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))

48 <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))

48 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

49 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))