on master help sign in
Fix parser for :def REPL command
fc5a9cbbmsherman
src/Idris/REPLParser.hs+1−1
@@ -61,7 +61,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)
61 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))
61 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))
62 <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))
62 <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))
63 <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))
63 <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))
64− <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))
64+ <|> try (do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n))
65 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))
65 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))
66 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))
66 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))
67 <|> try (do cmd ["u", "universes"]; eof; return Universes)
67 <|> try (do cmd ["u", "universes"]; eof; return Universes)