Idris.IdeMode

Synopsis

• parseMessage :: String -> Either Err (SExp, Integer)
• convSExp :: SExpable a => String -> a -> Integer -> String
• data WhatDocs
  • = Overview
  • | Full
• data IdeModeCommand
  • = REPLCompletions String
  • | Interpret String
  • | TypeOf String
  • | CaseSplit Int String
  • | AddClause Int String
  • | AddProofClause Int String
  • | AddMissing Int String
  • | MakeWithBlock Int String
  • | ProofSearch Bool Int String [String] (Maybe Int)
  • | MakeLemma Int String
  • | LoadFile String (Maybe Int)
  • | DocsFor String WhatDocs
  • | Apropos String
  • | GetOpts
  • | SetOpt Opt Bool
  • | Metavariables Int
  • | WhoCalls String
  • | CallsWho String
  • | BrowseNS String
  • | TermNormalise [(Name, Bool)] Term
  • | TermShowImplicits [(Name, Bool)] Term
  • | TermNoImplicits [(Name, Bool)] Term
  • | TermElab [(Name, Bool)] Term
  • | PrintDef String
  • | ErrString Err
  • | ErrPPrint Err
  • | GetIdrisVersion
• sexpToCommand :: SExp -> Maybe IdeModeCommand
• data SExp
  • = SexpList [SExp]
  • | StringAtom String
  • | BoolAtom Bool
  • | IntegerAtom Integer
  • | SymbolAtom String
• class SExpable a where
  • toSExp :: a -> SExp
• data Opt
  • = ShowImpl
  • | ErrContext
• ideModeEpoch :: Int
• getLen :: Handle -> IO (Either Err Int)
• getNChar :: Handle -> Int -> String -> IO String

Documentation