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

src/Idris/AbsSyntaxTree.hs−1

compare with master

unifiedsplit

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

285 | HNF PTerm

286 | TestInline PTerm

287 | Defn Name

288− | Info Name

289 | Missing Name

288 | Missing Name

290 | DynamicLink FilePath

289 | DynamicLink FilePath

291 | ListDynamic

290 | ListDynamic

src/Idris/Help.hs−1

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

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

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

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

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

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

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

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

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

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

40 ([":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)

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

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

388 iPrintResult ""

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

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

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

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

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

392-- RmProof and AddProof not supported!

391-- RmProof and AddProof not supported!

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

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

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

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

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

692 iputStrLn (show cg')

691 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"

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

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

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

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

701process h fn (CaseSplitAt updatefile l n)

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

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

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

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

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

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

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

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

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

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