6a99256 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove the REPL Info command

Removed from the `Command` datastructure, REPL-parser, REPL-help, process and ideslaveProcess. The functionality of showing infos for typeclasses has been subsumed by the `DocStr` command.

commit6a99256246008ba232791c9236e7c03a465b3d6a authorPaul Koerbitz <paul.koerbitz@theppro.com> dateThu 1 May 2014, 01:06 (12 years ago) parent71bdbbb

4 files changed−10

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs−1 src/Idris/Help.hs−1 src/Idris/REPL.hs−7 src/Idris/REPLParser.hs−1

src/Idris/AbsSyntaxTree.hs−1

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

285285 | HNF PTerm

286286 | TestInline PTerm

287287 | Defn Name

288− | Info Name

289288 | Missing Name

290289 | DynamicLink FilePath

291290 | ListDynamic

src/Idris/Help.hs−1

@@ -35,7 +35,6 @@ help =

3535 ([":apropos"], NoArg, "Search names, types, and documentation"),

3636 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

3737 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38− ([":i", ":info"], NameArg, "Display information about a type class"),

3938 ([":total"], NameArg, "Check the totality of a name"),

4039 ([":r",":reload"], NoArg, "Reload current file"),

4140 ([":l",":load"], FileArg, "Load a new file"),

src/Idris/REPL.hs−7

@@ -386,7 +386,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

386386ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

387387ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

388388 iPrintResult ""

389−ideslaveProcess fn (Info n) = process stdout fn (Info n)

390389ideslaveProcess fn (Search t) = process stdout fn (Search t)

391390ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

392391-- RmProof and AddProof not supported!

@@ -690,12 +689,6 @@ process h fn (DebugInfo n)

690689 iputStrLn $ "Size change: " ++ show sc

691690 when (not (null cg')) $ do iputStrLn "Call graph:\n"

692691 iputStrLn (show cg')

693−process h fn (Info n)

694− = do i <- getIState

695− case lookupCtxt n (idris_classes i) of

696− [c] -> do info <- classInfo c

697− ihRenderResult h info

698− _ -> iPrintError "Not a class"

699692process h fn (Search t) = iPrintError "Not implemented"

700693-- FIXME: There is far too much repetition in the cases below!

701694process h fn (CaseSplitAt updatefile l n)

src/Idris/REPLParser.hs−1

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

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

6060 <|> try (do cmd ["u", "universes"]; eof; return Universes)

6161 <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

62− <|> try (do cmd ["i", "info"]; n <- P.fnName; eof; return (Info n))

6362 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

6463 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

6564 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))