Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- newtype Type = Type Text
- newtype Message = Message {
- getMessage :: Text
- data Response
- = DisplayInfo DisplayInfo
- | ClearHighlighting
- | HighlightingInfo Bool [Highlight]
- | ClearRunningInfo
- | RunningInfo Int Text
- | Status { }
- | JumpToError FilePath AgdaIndex
- | InteractionPoints [InteractionPoint Maybe]
- | GiveAction Text (InteractionPoint (Const ()))
- | MakeCase MakeCase
- | SolveAll [Solution]
- | Unknown Text Value
- data Agda = Agda {}
- data BufferStuff = BufferStuff {}
- data InteractionPoint f = InteractionPoint {}
- newtype Extmark = Extmark Int64
- data DefinitionSite = DefinitionSite {}
- data DisplayInfo
- = AllGoalsWarnings {
- di_all_visible :: [GoalInfo (InteractionPoint Identity)]
- di_all_invisible :: [GoalInfo NamedPoint]
- di_errors :: [Message]
- di_warnings :: [Message]
- | GoalSpecific {
- di_ips :: InteractionPoint Identity
- di_in_scope :: [InScope]
- di_type :: Type
- di_type_aux :: Maybe Type
- di_boundary :: Maybe [Text]
- di_output_forms :: Maybe [Text]
- | HelperFunction Text
- | InferredType Type
- | DisplayError Text
- | WhyInScope Text
- | NormalForm Text
- | UnknownDisplayInfo Value
- = AllGoalsWarnings {
- newtype InfoBuffer = InfoBuffer {}
- newtype LineIntervals = LineIntervals {}
- data CornelisState = CornelisState {}
- type BufferNum = Int64
- type Diff0 = Diff DPos
- data SplitLocation
- data CornelisConfig = CornelisConfig {}
- data CornelisEnv = CornelisEnv {}
- data AgdaResp = AgdaResp {}
- data Highlight = Highlight {}
- data MakeCase = RegularCase MakeCaseVariant [Text] (InteractionPoint Identity)
- data Solution = Solution {}
- data MakeCaseVariant
- data NamedPoint = NamedPoint {}
- newtype AgdaPos' = AgdaPos AgdaPos
- data GoalInfo a = GoalInfo {}
- data InScope = InScope {
- is_refied_name :: Text
- is_original_name :: Text
- is_in_scope :: Bool
- is_type :: Type
- newtype TypeAux = TypeAux {}
- data ExtmarkStuff = ExtmarkStuff {}
- data DebugCommand = DumpIPs
- type DPos = Colline (LineNumber 'ZeroIndexed) VimIndex
- readSplitLocation :: String -> Maybe SplitLocation
- ip_interval' :: InteractionPoint Identity -> AgdaInterval
- sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity)
- data InteractionId
- data Buffer
- data Window
- data Text
- traceMX :: Show a => String -> a -> Neovim env ()
- type HasCallStack = ?callStack :: CallStack
Documentation
Instances
Generic Agda Source # | |
type Rep Agda Source # | |
Defined in Cornelis.Types type Rep Agda = D1 ('MetaData "Agda" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "Agda" 'PrefixI 'True) ((S1 ('MetaSel ('Just "a_buffer") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Buffer) :*: S1 ('MetaSel ('Just "a_ready") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IORef Bool))) :*: (S1 ('MetaSel ('Just "a_req") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (InChan String)) :*: S1 ('MetaSel ('Just "a_hdl") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProcessHandle)))) |
data BufferStuff Source #
Instances
data InteractionPoint f Source #
Instances
data DefinitionSite Source #
Instances
FromJSON DefinitionSite Source # | |
Defined in Cornelis.Types parseJSON :: Value -> Parser DefinitionSite # parseJSONList :: Value -> Parser [DefinitionSite] # | |
Show DefinitionSite Source # | |
Defined in Cornelis.Types showsPrec :: Int -> DefinitionSite -> ShowS # show :: DefinitionSite -> String # showList :: [DefinitionSite] -> ShowS # | |
Eq DefinitionSite Source # | |
Defined in Cornelis.Types (==) :: DefinitionSite -> DefinitionSite -> Bool # (/=) :: DefinitionSite -> DefinitionSite -> Bool # | |
Ord DefinitionSite Source # | |
Defined in Cornelis.Types compare :: DefinitionSite -> DefinitionSite -> Ordering # (<) :: DefinitionSite -> DefinitionSite -> Bool # (<=) :: DefinitionSite -> DefinitionSite -> Bool # (>) :: DefinitionSite -> DefinitionSite -> Bool # (>=) :: DefinitionSite -> DefinitionSite -> Bool # max :: DefinitionSite -> DefinitionSite -> DefinitionSite # min :: DefinitionSite -> DefinitionSite -> DefinitionSite # |
data DisplayInfo Source #
Instances
newtype InfoBuffer Source #
Instances
Generic InfoBuffer Source # | |
Defined in Cornelis.Types type Rep InfoBuffer :: Type -> Type # from :: InfoBuffer -> Rep InfoBuffer x # to :: Rep InfoBuffer x -> InfoBuffer # | |
type Rep InfoBuffer Source # | |
Defined in Cornelis.Types type Rep InfoBuffer = D1 ('MetaData "InfoBuffer" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'True) (C1 ('MetaCons "InfoBuffer" 'PrefixI 'True) (S1 ('MetaSel ('Just "iw_buffer") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Buffer))) |
newtype LineIntervals Source #
Data for mapping code point indices to byte indices
LineIntervals | |
|
Instances
Monoid LineIntervals Source # | |
Defined in Cornelis.Types mempty :: LineIntervals # mappend :: LineIntervals -> LineIntervals -> LineIntervals # mconcat :: [LineIntervals] -> LineIntervals # | |
Semigroup LineIntervals Source # | |
Defined in Cornelis.Types (<>) :: LineIntervals -> LineIntervals -> LineIntervals # sconcat :: NonEmpty LineIntervals -> LineIntervals # stimes :: Integral b => b -> LineIntervals -> LineIntervals # |
data CornelisState Source #
Instances
Generic CornelisState Source # | |
Defined in Cornelis.Types type Rep CornelisState :: Type -> Type # from :: CornelisState -> Rep CornelisState x # to :: Rep CornelisState x -> CornelisState # | |
MonadState CornelisState (Neovim CornelisEnv) Source # | |
Defined in Cornelis.Types get :: Neovim CornelisEnv CornelisState # put :: CornelisState -> Neovim CornelisEnv () # state :: (CornelisState -> (a, CornelisState)) -> Neovim CornelisEnv a # | |
type Rep CornelisState Source # | |
Defined in Cornelis.Types type Rep CornelisState = D1 ('MetaData "CornelisState" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "CornelisState" 'PrefixI 'True) (S1 ('MetaSel ('Just "cs_buffers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Buffer BufferStuff)) :*: S1 ('MetaSel ('Just "cs_diff") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map BufferNum Diff0)))) |
type BufferNum = Int64 Source #
Buffer update events give us this instead of a proper Buffer There is buffer_get_number :: Buffer -> Neovim env BufferNum but nothing the other way???
data SplitLocation Source #
Instances
data CornelisConfig Source #
Instances
Generic CornelisConfig Source # | |
Defined in Cornelis.Types type Rep CornelisConfig :: Type -> Type # from :: CornelisConfig -> Rep CornelisConfig x # to :: Rep CornelisConfig x -> CornelisConfig # | |
Show CornelisConfig Source # | |
Defined in Cornelis.Types showsPrec :: Int -> CornelisConfig -> ShowS # show :: CornelisConfig -> String # showList :: [CornelisConfig] -> ShowS # | |
type Rep CornelisConfig Source # | |
Defined in Cornelis.Types type Rep CornelisConfig = D1 ('MetaData "CornelisConfig" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "CornelisConfig" 'PrefixI 'True) (S1 ('MetaSel ('Just "cc_max_height") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int64) :*: (S1 ('MetaSel ('Just "cc_max_width") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int64) :*: S1 ('MetaSel ('Just "cc_split_location") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SplitLocation)))) |
data CornelisEnv Source #
Instances
Instances
Generic AgdaResp Source # | |
type Rep AgdaResp Source # | |
Defined in Cornelis.Types type Rep AgdaResp = D1 ('MetaData "AgdaResp" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "AgdaResp" 'PrefixI 'True) (S1 ('MetaSel ('Just "ar_buffer") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Buffer) :*: S1 ('MetaSel ('Just "ar_message") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Response))) |
Highlight | |
|
Instances
FromJSON MakeCase Source # | |
Defined in Cornelis.Types | |
Generic MakeCase Source # | |
Show MakeCase Source # | |
Eq MakeCase Source # | |
Ord MakeCase Source # | |
Defined in Cornelis.Types | |
type Rep MakeCase Source # | |
Defined in Cornelis.Types type Rep MakeCase = D1 ('MetaData "MakeCase" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "RegularCase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MakeCaseVariant) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (InteractionPoint Identity))))) |
data MakeCaseVariant Source #
Instances
data NamedPoint Source #
Instances
FromJSON NamedPoint Source # | |
Defined in Cornelis.Types parseJSON :: Value -> Parser NamedPoint # parseJSONList :: Value -> Parser [NamedPoint] # | |
Show NamedPoint Source # | |
Defined in Cornelis.Types showsPrec :: Int -> NamedPoint -> ShowS # show :: NamedPoint -> String # showList :: [NamedPoint] -> ShowS # | |
Eq NamedPoint Source # | |
Defined in Cornelis.Types (==) :: NamedPoint -> NamedPoint -> Bool # (/=) :: NamedPoint -> NamedPoint -> Bool # | |
Ord NamedPoint Source # | |
Defined in Cornelis.Types compare :: NamedPoint -> NamedPoint -> Ordering # (<) :: NamedPoint -> NamedPoint -> Bool # (<=) :: NamedPoint -> NamedPoint -> Bool # (>) :: NamedPoint -> NamedPoint -> Bool # (>=) :: NamedPoint -> NamedPoint -> Bool # max :: NamedPoint -> NamedPoint -> NamedPoint # min :: NamedPoint -> NamedPoint -> NamedPoint # |
Instances
Functor GoalInfo Source # | |
FromJSON a => FromJSON (GoalInfo a) Source # | |
Defined in Cornelis.Types | |
Show a => Show (GoalInfo a) Source # | |
Eq a => Eq (GoalInfo a) Source # | |
Ord a => Ord (GoalInfo a) Source # | |
InScope | |
|
data ExtmarkStuff Source #
Instances
Show ExtmarkStuff Source # | |
Defined in Cornelis.Types showsPrec :: Int -> ExtmarkStuff -> ShowS # show :: ExtmarkStuff -> String # showList :: [ExtmarkStuff] -> ShowS # | |
Eq ExtmarkStuff Source # | |
Defined in Cornelis.Types (==) :: ExtmarkStuff -> ExtmarkStuff -> Bool # (/=) :: ExtmarkStuff -> ExtmarkStuff -> Bool # | |
Ord ExtmarkStuff Source # | |
Defined in Cornelis.Types compare :: ExtmarkStuff -> ExtmarkStuff -> Ordering # (<) :: ExtmarkStuff -> ExtmarkStuff -> Bool # (<=) :: ExtmarkStuff -> ExtmarkStuff -> Bool # (>) :: ExtmarkStuff -> ExtmarkStuff -> Bool # (>=) :: ExtmarkStuff -> ExtmarkStuff -> Bool # max :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff # min :: ExtmarkStuff -> ExtmarkStuff -> ExtmarkStuff # |
data DebugCommand Source #
Instances
type DPos = Colline (LineNumber 'ZeroIndexed) VimIndex Source #
sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity) Source #
data InteractionId Source #
Instances
Instances
Generic Buffer | |
Show Buffer | |
NFData Buffer | |
Defined in Neovim.API.Text | |
Eq Buffer | |
Ord Buffer Source # | |
NvimObject Buffer | |
type Rep Buffer | |
Defined in Neovim.API.Text type Rep Buffer = D1 ('MetaData "Buffer" "Neovim.API.Text" "nvim-hs-2.3.2.3-EiEXbDxSBLL2xZh1tUwc4J" 'False) (C1 ('MetaCons "Buffer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ByteString))) |
Instances
Generic Window | |
Show Window | |
NFData Window | |
Defined in Neovim.API.Text | |
Eq Window | |
NvimObject Window | |
type Rep Window | |
Defined in Neovim.API.Text type Rep Window = D1 ('MetaData "Window" "Neovim.API.Text" "nvim-hs-2.3.2.3-EiEXbDxSBLL2xZh1tUwc4J" 'False) (C1 ('MetaCons "Window" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ByteString))) |
A space efficient, packed, unboxed Unicode text type.
Instances
type HasCallStack = ?callStack :: CallStack #
Request a CallStack.
NOTE: The implicit parameter ?callStack :: CallStack
is an
implementation detail and should not be considered part of the
CallStack
API, we may decide to change the implementation in the
future.
Since: base-4.9.0.0
Orphan instances
FromJSON AgdaInterval Source # | |
parseJSON :: Value -> Parser AgdaInterval # parseJSONList :: Value -> Parser [AgdaInterval] # | |
Ord Buffer Source # | |