31ca891 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parse _|_ as a name in :doc

Fixes #1128.

commit31ca891c87fface83bcdfffeb93c95bcb3e8b8ca authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 30 Apr 2014, 17:29 (12 years ago) parent5265109

3 files changed+4−1

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Docs.hs+2 src/Idris/REPLParser.hs+1−1

src/Idris/AbsSyntaxTree.hs+1

@@ -1384,6 +1384,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

13841384 where strName (UN n) = T.unpack n

13851385 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

13861386 | otherwise = strName n

1387+ strName n | n == falseTy = "_|_"

13871388 strName (MN i s) = T.unpack s

13881389 strName other = show other

13891390

src/Idris/Docs.hs+2

@@ -120,6 +120,8 @@ docFun n

120120 where funName :: Name -> String

121121 funName (UN n) = str n

122122 funName (NS n _) = funName n

123+ funName n

124+ | n == falseTy = "_|_"

123125

124126getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

125127getPArgNames (PPi plicity name ty body) ds =

src/Idris/REPLParser.hs+1−1

@@ -50,7 +50,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

5050 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

5151 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

5252 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

53− <|> try (do cmd ["doc"]; n <- P.fnName; eof; return (DocStr n))

53+ <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr n))

5454 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

5555 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

5656 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))