34e25c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1135 from david-christiansen/nicola-stuff

Comments in .ipkg files and :doc works for _|_

commit34e25c2f53209c67db1f9bf2c694d8d9cd7bae86 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 30 Apr 2014, 21:47 (12 years ago) parent92dcd22 31ca891

4 files changed+6−1

compare with master

unifiedsplit

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

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

src/Pkg/PParser.hs+2

@@ -78,4 +78,6 @@ pClause = do reserved "executable"; lchar '=';

7878 mk <- iName []

7979 st <- get

8080 put (st { makefile = Just (show mk) })

81+ <|> do string "--"; many (satisfy (not . isEol)) ; satisfy isEol

82+ return ()

8183