Cornelis.Types

Documentation

newtype Type

Constructors

Type Text

Instances

FromJSON Type

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser Type

parseJSONList :: Value -> Parser [Type]

omittedField :: Maybe Type

Show Type

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Eq Type

Defined in Cornelis.Types

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Ord Type

Defined in Cornelis.Types

Methods

compare :: Type -> Type -> Ordering

(<) :: Type -> Type -> Bool

(<=) :: Type -> Type -> Bool

(>) :: Type -> Type -> Bool

(>=) :: Type -> Type -> Bool

max :: Type -> Type -> Type

min :: Type -> Type -> Type

newtype Message

Constructors

Message

Fields

• getMessage :: Text

Instances

FromJSON Message

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser Message

parseJSONList :: Value -> Parser [Message]

omittedField :: Maybe Message

Show Message

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Message -> ShowS

show :: Message -> String

showList :: [Message] -> ShowS

Eq Message

Defined in Cornelis.Types

Methods

(==) :: Message -> Message -> Bool

(/=) :: Message -> Message -> Bool

Ord Message

Defined in Cornelis.Types

Methods

compare :: Message -> Message -> Ordering

(<) :: Message -> Message -> Bool

(<=) :: Message -> Message -> Bool

(>) :: Message -> Message -> Bool

(>=) :: Message -> Message -> Bool

max :: Message -> Message -> Message

min :: Message -> Message -> Message

data Response

Constructors

DisplayInfo DisplayInfo

ClearHighlighting

HighlightingInfo Bool [Highlight]

ClearRunningInfo

RunningInfo Int Text

Status

Fields

• status_checked :: Bool
• status_showIrrelevant :: Bool
• status_showImplicits :: Bool

JumpToError FilePath AgdaIndex

InteractionPoints [InteractionPoint Maybe]

GiveAction Text (InteractionPoint (Const ()))

MakeCase MakeCase

SolveAll [Solution]

Unknown Text Value

Instances

FromJSON Response

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser Response

parseJSONList :: Value -> Parser [Response]

omittedField :: Maybe Response

Show Response

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Response -> ShowS

show :: Response -> String

showList :: [Response] -> ShowS

Eq Response

Defined in Cornelis.Types

Methods

(==) :: Response -> Response -> Bool

(/=) :: Response -> Response -> Bool

Ord Response

Defined in Cornelis.Types

Methods

compare :: Response -> Response -> Ordering

(<) :: Response -> Response -> Bool

(<=) :: Response -> Response -> Bool

(>) :: Response -> Response -> Bool

(>=) :: Response -> Response -> Bool

max :: Response -> Response -> Response

min :: Response -> Response -> Response

data Agda

Constructors

Agda

Fields

• a_buffer :: Buffer
• a_ready :: IORef Bool
• a_req :: InChan String
• a_hdl :: ProcessHandle

Instances

Generic Agda

Defined in Cornelis.Types

Associated Types

type Rep Agda :: Type -> Type

Methods

from :: Agda -> Rep Agda x

to :: Rep Agda x -> Agda

type Rep Agda

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

Constructors

BufferStuff

Fields

• bs_agda_proc :: Agda
• bs_ips :: Map InteractionId (InteractionPoint Identity)
• bs_ip_exts :: Map InteractionId Extmark
• bs_goto_sites :: Map Extmark DefinitionSite
• bs_goals :: DisplayInfo
• bs_info_win :: InfoBuffer
• bs_code_map :: LineIntervals

Instances

Generic BufferStuff

Defined in Cornelis.Types

Associated Types

type Rep BufferStuff :: Type -> Type

Methods

from :: BufferStuff -> Rep BufferStuff x

to :: Rep BufferStuff x -> BufferStuff

type Rep BufferStuff

Defined in Cornelis.Types

type Rep BufferStuff = D1 ('MetaData "BufferStuff" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "BufferStuff" 'PrefixI 'True) ((S1 ('MetaSel ('Just "bs_agda_proc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Agda) :*: (S1 ('MetaSel ('Just "bs_ips") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map InteractionId (InteractionPoint Identity))) :*: S1 ('MetaSel ('Just "bs_ip_exts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map InteractionId Extmark)))) :*: ((S1 ('MetaSel ('Just "bs_goto_sites") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Extmark DefinitionSite)) :*: S1 ('MetaSel ('Just "bs_goals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DisplayInfo)) :*: (S1 ('MetaSel ('Just "bs_info_win") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InfoBuffer) :*: S1 ('MetaSel ('Just "bs_code_map") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LineIntervals)))))

data InteractionPoint f

Constructors

InteractionPoint

Fields

• ip_id :: InteractionId
• ip_intervalM :: f AgdaInterval

Instances

FromJSON (InteractionPoint (Const () :: Type -> Type))

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser (InteractionPoint (Const ()))

parseJSONList :: Value -> Parser [InteractionPoint (Const ())]

omittedField :: Maybe (InteractionPoint (Const ()))

FromJSON (InteractionPoint Identity)

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser (InteractionPoint Identity)

parseJSONList :: Value -> Parser [InteractionPoint Identity]

omittedField :: Maybe (InteractionPoint Identity)

FromJSON (InteractionPoint Maybe)

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser (InteractionPoint Maybe)

parseJSONList :: Value -> Parser [InteractionPoint Maybe]

omittedField :: Maybe (InteractionPoint Maybe)

Generic (InteractionPoint f)

Defined in Cornelis.Types

Associated Types

type Rep (InteractionPoint f) :: Type -> Type

Methods

from :: InteractionPoint f -> Rep (InteractionPoint f) x

to :: Rep (InteractionPoint f) x -> InteractionPoint f

Show (f AgdaInterval) => Show (InteractionPoint f)

Defined in Cornelis.Types

Methods

showsPrec :: Int -> InteractionPoint f -> ShowS

show :: InteractionPoint f -> String

showList :: [InteractionPoint f] -> ShowS

Eq (f AgdaInterval) => Eq (InteractionPoint f)

Defined in Cornelis.Types

Methods

(==) :: InteractionPoint f -> InteractionPoint f -> Bool

(/=) :: InteractionPoint f -> InteractionPoint f -> Bool

Ord (f AgdaInterval) => Ord (InteractionPoint f)

Defined in Cornelis.Types

Methods

compare :: InteractionPoint f -> InteractionPoint f -> Ordering

(<) :: InteractionPoint f -> InteractionPoint f -> Bool

(<=) :: InteractionPoint f -> InteractionPoint f -> Bool

(>) :: InteractionPoint f -> InteractionPoint f -> Bool

(>=) :: InteractionPoint f -> InteractionPoint f -> Bool

max :: InteractionPoint f -> InteractionPoint f -> InteractionPoint f

min :: InteractionPoint f -> InteractionPoint f -> InteractionPoint f

type Rep (InteractionPoint f)

Defined in Cornelis.Types

type Rep (InteractionPoint f) = D1 ('MetaData "InteractionPoint" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "InteractionPoint" 'PrefixI 'True) (S1 ('MetaSel ('Just "ip_id") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId) :*: S1 ('MetaSel ('Just "ip_intervalM") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f AgdaInterval))))

newtype Extmark

Constructors

Extmark Int64

Instances

Show Extmark

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Extmark -> ShowS

show :: Extmark -> String

showList :: [Extmark] -> ShowS

Eq Extmark

Defined in Cornelis.Types

Methods

(==) :: Extmark -> Extmark -> Bool

(/=) :: Extmark -> Extmark -> Bool

Ord Extmark

Defined in Cornelis.Types

Methods

compare :: Extmark -> Extmark -> Ordering

(<) :: Extmark -> Extmark -> Bool

(<=) :: Extmark -> Extmark -> Bool

(>) :: Extmark -> Extmark -> Bool

(>=) :: Extmark -> Extmark -> Bool

max :: Extmark -> Extmark -> Extmark

min :: Extmark -> Extmark -> Extmark

data DefinitionSite

Constructors

DefinitionSite

Fields

• ds_filepath :: Text
• ds_position :: AgdaIndex

Instances

FromJSON DefinitionSite

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser DefinitionSite

parseJSONList :: Value -> Parser [DefinitionSite]

omittedField :: Maybe DefinitionSite

Show DefinitionSite

Defined in Cornelis.Types

Methods

showsPrec :: Int -> DefinitionSite -> ShowS

show :: DefinitionSite -> String

showList :: [DefinitionSite] -> ShowS

Eq DefinitionSite

Defined in Cornelis.Types

Methods

(==) :: DefinitionSite -> DefinitionSite -> Bool

(/=) :: DefinitionSite -> DefinitionSite -> Bool

Ord DefinitionSite

Defined in Cornelis.Types

Methods

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

Constructors

AllGoalsWarnings

Fields

• di_all_visible :: [GoalInfo (InteractionPoint Identity)]
• di_all_invisible :: [GoalInfo NamedPoint]
• di_errors :: [Message]
• di_warnings :: [Message]

GoalSpecific

Fields

• 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

Instances

FromJSON DisplayInfo

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser DisplayInfo

parseJSONList :: Value -> Parser [DisplayInfo]

omittedField :: Maybe DisplayInfo

Generic DisplayInfo

Defined in Cornelis.Types

Associated Types

type Rep DisplayInfo :: Type -> Type

Methods

from :: DisplayInfo -> Rep DisplayInfo x

to :: Rep DisplayInfo x -> DisplayInfo

Show DisplayInfo

Defined in Cornelis.Types

Methods

showsPrec :: Int -> DisplayInfo -> ShowS

show :: DisplayInfo -> String

showList :: [DisplayInfo] -> ShowS

Eq DisplayInfo

Defined in Cornelis.Types

Methods

(==) :: DisplayInfo -> DisplayInfo -> Bool

(/=) :: DisplayInfo -> DisplayInfo -> Bool

Ord DisplayInfo

Defined in Cornelis.Types

Methods

compare :: DisplayInfo -> DisplayInfo -> Ordering

(<) :: DisplayInfo -> DisplayInfo -> Bool

(<=) :: DisplayInfo -> DisplayInfo -> Bool

(>) :: DisplayInfo -> DisplayInfo -> Bool

(>=) :: DisplayInfo -> DisplayInfo -> Bool

max :: DisplayInfo -> DisplayInfo -> DisplayInfo

min :: DisplayInfo -> DisplayInfo -> DisplayInfo

type Rep DisplayInfo

Defined in Cornelis.Types

type Rep DisplayInfo = D1 ('MetaData "DisplayInfo" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (((C1 ('MetaCons "AllGoalsWarnings" 'PrefixI 'True) ((S1 ('MetaSel ('Just "di_all_visible") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GoalInfo (InteractionPoint Identity)]) :*: S1 ('MetaSel ('Just "di_all_invisible") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GoalInfo NamedPoint])) :*: (S1 ('MetaSel ('Just "di_errors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Message]) :*: S1 ('MetaSel ('Just "di_warnings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Message]))) :+: C1 ('MetaCons "GoalSpecific" 'PrefixI 'True) ((S1 ('MetaSel ('Just "di_ips") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (InteractionPoint Identity)) :*: (S1 ('MetaSel ('Just "di_in_scope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [InScope]) :*: S1 ('MetaSel ('Just "di_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :*: (S1 ('MetaSel ('Just "di_type_aux") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Type)) :*: (S1 ('MetaSel ('Just "di_boundary") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Text])) :*: S1 ('MetaSel ('Just "di_output_forms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Text])))))) :+: (C1 ('MetaCons "HelperFunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "InferredType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: ((C1 ('MetaCons "DisplayError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "WhyInScope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))) :+: (C1 ('MetaCons "NormalForm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "UnknownDisplayInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Value)))))

newtype InfoBuffer

Constructors

InfoBuffer

Fields

• iw_buffer :: Buffer

Instances

Generic InfoBuffer

Defined in Cornelis.Types

Associated Types

type Rep InfoBuffer :: Type -> Type

Methods

from :: InfoBuffer -> Rep InfoBuffer x

to :: Rep InfoBuffer x -> InfoBuffer

type Rep InfoBuffer

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

Data for mapping code point indices to byte indices

Constructors

LineIntervals

Fields

• li_intervalMap :: IntervalMap AgdaIndex (LineNumber 'ZeroIndexed, Text)

  Mapping from positions to line numbers

Instances

Monoid LineIntervals

Defined in Cornelis.Types

Methods

mempty :: LineIntervals

mappend :: LineIntervals -> LineIntervals -> LineIntervals

mconcat :: [LineIntervals] -> LineIntervals

Semigroup LineIntervals

Defined in Cornelis.Types

Methods

(<>) :: LineIntervals -> LineIntervals -> LineIntervals

sconcat :: NonEmpty LineIntervals -> LineIntervals

stimes :: Integral b => b -> LineIntervals -> LineIntervals

data CornelisState

Constructors

CornelisState

Fields

• cs_buffers :: Map Buffer BufferStuff
• cs_diff :: Map BufferNum Diff0

Instances

Generic CornelisState

Defined in Cornelis.Types

Associated Types

type Rep CornelisState :: Type -> Type

Methods

from :: CornelisState -> Rep CornelisState x

to :: Rep CornelisState x -> CornelisState

MonadState CornelisState (Neovim CornelisEnv)

Defined in Cornelis.Types

Methods

get :: Neovim CornelisEnv CornelisState

put :: CornelisState -> Neovim CornelisEnv ()

state :: (CornelisState -> (a, CornelisState)) -> Neovim CornelisEnv a

type Rep CornelisState

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

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???

type Diff0 = Diff DPos

data SplitLocation

Constructors

Vertical

Horizontal

OnLeft

OnRight

OnTop

OnBottom

Instances

Bounded SplitLocation

Defined in Cornelis.Types

Methods

minBound :: SplitLocation

maxBound :: SplitLocation

Enum SplitLocation

Defined in Cornelis.Types

Methods

succ :: SplitLocation -> SplitLocation

pred :: SplitLocation -> SplitLocation

toEnum :: Int -> SplitLocation

fromEnum :: SplitLocation -> Int

enumFrom :: SplitLocation -> [SplitLocation]

enumFromThen :: SplitLocation -> SplitLocation -> [SplitLocation]

enumFromTo :: SplitLocation -> SplitLocation -> [SplitLocation]

enumFromThenTo :: SplitLocation -> SplitLocation -> SplitLocation -> [SplitLocation]

Show SplitLocation

Defined in Cornelis.Types

Methods

showsPrec :: Int -> SplitLocation -> ShowS

show :: SplitLocation -> String

showList :: [SplitLocation] -> ShowS

Eq SplitLocation

Defined in Cornelis.Types

Methods

(==) :: SplitLocation -> SplitLocation -> Bool

(/=) :: SplitLocation -> SplitLocation -> Bool

Ord SplitLocation

Defined in Cornelis.Types

Methods

compare :: SplitLocation -> SplitLocation -> Ordering

(<) :: SplitLocation -> SplitLocation -> Bool

(<=) :: SplitLocation -> SplitLocation -> Bool

(>) :: SplitLocation -> SplitLocation -> Bool

(>=) :: SplitLocation -> SplitLocation -> Bool

max :: SplitLocation -> SplitLocation -> SplitLocation

min :: SplitLocation -> SplitLocation -> SplitLocation

data CornelisConfig

Constructors

CornelisConfig

Fields

• cc_max_height :: Int64
• cc_max_width :: Int64
• cc_split_location :: SplitLocation

Instances

Generic CornelisConfig

Defined in Cornelis.Types

Associated Types

type Rep CornelisConfig :: Type -> Type

Methods

from :: CornelisConfig -> Rep CornelisConfig x

to :: Rep CornelisConfig x -> CornelisConfig

Show CornelisConfig

Defined in Cornelis.Types

Methods

showsPrec :: Int -> CornelisConfig -> ShowS

show :: CornelisConfig -> String

showList :: [CornelisConfig] -> ShowS

type Rep CornelisConfig

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

Constructors

CornelisEnv

Fields

• ce_state :: IORef CornelisState
• ce_stream :: InChan AgdaResp
• ce_namespace :: Int64
• ce_config :: CornelisConfig

Instances

Generic CornelisEnv

Defined in Cornelis.Types

Associated Types

type Rep CornelisEnv :: Type -> Type

Methods

from :: CornelisEnv -> Rep CornelisEnv x

to :: Rep CornelisEnv x -> CornelisEnv

MonadState CornelisState (Neovim CornelisEnv)

Defined in Cornelis.Types

Methods

get :: Neovim CornelisEnv CornelisState

put :: CornelisState -> Neovim CornelisEnv ()

state :: (CornelisState -> (a, CornelisState)) -> Neovim CornelisEnv a

type Rep CornelisEnv

Defined in Cornelis.Types

type Rep CornelisEnv = D1 ('MetaData "CornelisEnv" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "CornelisEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ce_state") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IORef CornelisState)) :*: S1 ('MetaSel ('Just "ce_stream") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (InChan AgdaResp))) :*: (S1 ('MetaSel ('Just "ce_namespace") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int64) :*: S1 ('MetaSel ('Just "ce_config") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CornelisConfig))))

data AgdaResp

Constructors

AgdaResp

Fields

• ar_buffer :: Buffer
• ar_message :: Response

Instances

Generic AgdaResp

Defined in Cornelis.Types

Associated Types

type Rep AgdaResp :: Type -> Type

Methods

from :: AgdaResp -> Rep AgdaResp x

to :: Rep AgdaResp x -> AgdaResp

type Rep AgdaResp

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

data Highlight

Constructors

Highlight

Fields

• hl_atoms :: [Text]
• hl_definitionSite :: Maybe DefinitionSite
• hl_start :: AgdaIndex
• hl_end :: AgdaIndex

Instances

FromJSON Highlight

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser Highlight

parseJSONList :: Value -> Parser [Highlight]

omittedField :: Maybe Highlight

Show Highlight

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Highlight -> ShowS

show :: Highlight -> String

showList :: [Highlight] -> ShowS

Eq Highlight

Defined in Cornelis.Types

Methods

(==) :: Highlight -> Highlight -> Bool

(/=) :: Highlight -> Highlight -> Bool

Ord Highlight

Defined in Cornelis.Types

Methods

compare :: Highlight -> Highlight -> Ordering

(<) :: Highlight -> Highlight -> Bool

(<=) :: Highlight -> Highlight -> Bool

(>) :: Highlight -> Highlight -> Bool

(>=) :: Highlight -> Highlight -> Bool

max :: Highlight -> Highlight -> Highlight

min :: Highlight -> Highlight -> Highlight

data MakeCase

Constructors

RegularCase MakeCaseVariant [Text] (InteractionPoint Identity)

Instances

FromJSON MakeCase

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser MakeCase

parseJSONList :: Value -> Parser [MakeCase]

omittedField :: Maybe MakeCase

Generic MakeCase

Defined in Cornelis.Types

Associated Types

type Rep MakeCase :: Type -> Type

Methods

from :: MakeCase -> Rep MakeCase x

to :: Rep MakeCase x -> MakeCase

Show MakeCase

Defined in Cornelis.Types

Methods

showsPrec :: Int -> MakeCase -> ShowS

show :: MakeCase -> String

showList :: [MakeCase] -> ShowS

Eq MakeCase

Defined in Cornelis.Types

Methods

(==) :: MakeCase -> MakeCase -> Bool

(/=) :: MakeCase -> MakeCase -> Bool

Ord MakeCase

Defined in Cornelis.Types

Methods

compare :: MakeCase -> MakeCase -> Ordering

(<) :: MakeCase -> MakeCase -> Bool

(<=) :: MakeCase -> MakeCase -> Bool

(>) :: MakeCase -> MakeCase -> Bool

(>=) :: MakeCase -> MakeCase -> Bool

max :: MakeCase -> MakeCase -> MakeCase

min :: MakeCase -> MakeCase -> MakeCase

type Rep MakeCase

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 Solution

Constructors

Solution

Fields

• s_ip :: InteractionId
• s_expression :: Text

Instances

FromJSON Solution

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser Solution

parseJSONList :: Value -> Parser [Solution]

omittedField :: Maybe Solution

Show Solution

Defined in Cornelis.Types

Methods

showsPrec :: Int -> Solution -> ShowS

show :: Solution -> String

showList :: [Solution] -> ShowS

Eq Solution

Defined in Cornelis.Types

Methods

(==) :: Solution -> Solution -> Bool

(/=) :: Solution -> Solution -> Bool

Ord Solution

Defined in Cornelis.Types

Methods

compare :: Solution -> Solution -> Ordering

(<) :: Solution -> Solution -> Bool

(<=) :: Solution -> Solution -> Bool

(>) :: Solution -> Solution -> Bool

(>=) :: Solution -> Solution -> Bool

max :: Solution -> Solution -> Solution

min :: Solution -> Solution -> Solution

data MakeCaseVariant

Constructors

Function

ExtendedLambda

Instances

FromJSON MakeCaseVariant

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser MakeCaseVariant

parseJSONList :: Value -> Parser [MakeCaseVariant]

omittedField :: Maybe MakeCaseVariant

Generic MakeCaseVariant

Defined in Cornelis.Types

Associated Types

type Rep MakeCaseVariant :: Type -> Type

Methods

from :: MakeCaseVariant -> Rep MakeCaseVariant x

to :: Rep MakeCaseVariant x -> MakeCaseVariant

Show MakeCaseVariant

Defined in Cornelis.Types

Methods

showsPrec :: Int -> MakeCaseVariant -> ShowS

show :: MakeCaseVariant -> String

showList :: [MakeCaseVariant] -> ShowS

Eq MakeCaseVariant

Defined in Cornelis.Types

Methods

(==) :: MakeCaseVariant -> MakeCaseVariant -> Bool

(/=) :: MakeCaseVariant -> MakeCaseVariant -> Bool

Ord MakeCaseVariant

Defined in Cornelis.Types

Methods

compare :: MakeCaseVariant -> MakeCaseVariant -> Ordering

(<) :: MakeCaseVariant -> MakeCaseVariant -> Bool

(<=) :: MakeCaseVariant -> MakeCaseVariant -> Bool

(>) :: MakeCaseVariant -> MakeCaseVariant -> Bool

(>=) :: MakeCaseVariant -> MakeCaseVariant -> Bool

max :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant

min :: MakeCaseVariant -> MakeCaseVariant -> MakeCaseVariant

type Rep MakeCaseVariant

Defined in Cornelis.Types

type Rep MakeCaseVariant = D1 ('MetaData "MakeCaseVariant" "Cornelis.Types" "cornelis-0.2.0.0-6a1gQdmcW6s9D29V5A3o0J" 'False) (C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendedLambda" 'PrefixI 'False) (U1 :: Type -> Type))

data NamedPoint

Constructors

NamedPoint

Fields

• np_name :: Text
• np_interval :: Maybe AgdaInterval

Instances

FromJSON NamedPoint

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser NamedPoint

parseJSONList :: Value -> Parser [NamedPoint]

omittedField :: Maybe NamedPoint

Show NamedPoint

Defined in Cornelis.Types

Methods

showsPrec :: Int -> NamedPoint -> ShowS

show :: NamedPoint -> String

showList :: [NamedPoint] -> ShowS

Eq NamedPoint

Defined in Cornelis.Types

Methods

(==) :: NamedPoint -> NamedPoint -> Bool

(/=) :: NamedPoint -> NamedPoint -> Bool

Ord NamedPoint

Defined in Cornelis.Types

Methods

compare :: NamedPoint -> NamedPoint -> Ordering

(<) :: NamedPoint -> NamedPoint -> Bool

(<=) :: NamedPoint -> NamedPoint -> Bool

(>) :: NamedPoint -> NamedPoint -> Bool

(>=) :: NamedPoint -> NamedPoint -> Bool

max :: NamedPoint -> NamedPoint -> NamedPoint

min :: NamedPoint -> NamedPoint -> NamedPoint

newtype AgdaPos'

Constructors

AgdaPos AgdaPos

Instances

FromJSON AgdaPos'

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser AgdaPos'

parseJSONList :: Value -> Parser [AgdaPos']

omittedField :: Maybe AgdaPos'

data GoalInfo a

Constructors

GoalInfo

Fields

• gi_ip :: a
• gi_type :: Type

Instances

Functor GoalInfo

Defined in Cornelis.Types

Methods

fmap :: (a -> b) -> GoalInfo a -> GoalInfo b

(<$) :: a -> GoalInfo b -> GoalInfo a

FromJSON a => FromJSON (GoalInfo a)

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser (GoalInfo a)

parseJSONList :: Value -> Parser [GoalInfo a]

omittedField :: Maybe (GoalInfo a)

Show a => Show (GoalInfo a)

Defined in Cornelis.Types

Methods

showsPrec :: Int -> GoalInfo a -> ShowS

show :: GoalInfo a -> String

showList :: [GoalInfo a] -> ShowS

Eq a => Eq (GoalInfo a)

Defined in Cornelis.Types

Methods

(==) :: GoalInfo a -> GoalInfo a -> Bool

(/=) :: GoalInfo a -> GoalInfo a -> Bool

Ord a => Ord (GoalInfo a)

Defined in Cornelis.Types

Methods

compare :: GoalInfo a -> GoalInfo a -> Ordering

(<) :: GoalInfo a -> GoalInfo a -> Bool

(<=) :: GoalInfo a -> GoalInfo a -> Bool

(>) :: GoalInfo a -> GoalInfo a -> Bool

(>=) :: GoalInfo a -> GoalInfo a -> Bool

max :: GoalInfo a -> GoalInfo a -> GoalInfo a

min :: GoalInfo a -> GoalInfo a -> GoalInfo a

data InScope

Constructors

InScope

Fields

• is_refied_name :: Text
• is_original_name :: Text
• is_in_scope :: Bool
• is_type :: Type

Instances

FromJSON InScope

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser InScope

parseJSONList :: Value -> Parser [InScope]

omittedField :: Maybe InScope

Show InScope

Defined in Cornelis.Types

Methods

showsPrec :: Int -> InScope -> ShowS

show :: InScope -> String

showList :: [InScope] -> ShowS

Eq InScope

Defined in Cornelis.Types

Methods

(==) :: InScope -> InScope -> Bool

(/=) :: InScope -> InScope -> Bool

Ord InScope

Defined in Cornelis.Types

Methods

compare :: InScope -> InScope -> Ordering

(<) :: InScope -> InScope -> Bool

(<=) :: InScope -> InScope -> Bool

(>) :: InScope -> InScope -> Bool

(>=) :: InScope -> InScope -> Bool

max :: InScope -> InScope -> InScope

min :: InScope -> InScope -> InScope

newtype TypeAux

Constructors

TypeAux

Fields

• ta_expr :: Type

Instances

FromJSON TypeAux

Defined in Cornelis.Types

Methods

parseJSON :: Value -> Parser TypeAux

parseJSONList :: Value -> Parser [TypeAux]

omittedField :: Maybe TypeAux

data ExtmarkStuff

Constructors

ExtmarkStuff

Fields

• es_mark :: Extmark
• es_hlgroup :: Text
• es_interval :: AgdaInterval

Instances

Show ExtmarkStuff

Defined in Cornelis.Types

Methods

showsPrec :: Int -> ExtmarkStuff -> ShowS

show :: ExtmarkStuff -> String

showList :: [ExtmarkStuff] -> ShowS

Eq ExtmarkStuff

Defined in Cornelis.Types

Methods

(==) :: ExtmarkStuff -> ExtmarkStuff -> Bool

(/=) :: ExtmarkStuff -> ExtmarkStuff -> Bool

Ord ExtmarkStuff

Defined in Cornelis.Types

Methods

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

Constructors

DumpIPs

Instances

Bounded DebugCommand

Defined in Cornelis.Types

Methods

minBound :: DebugCommand

maxBound :: DebugCommand

Enum DebugCommand

Defined in Cornelis.Types

Methods

succ :: DebugCommand -> DebugCommand

pred :: DebugCommand -> DebugCommand

toEnum :: Int -> DebugCommand

fromEnum :: DebugCommand -> Int

enumFrom :: DebugCommand -> [DebugCommand]

enumFromThen :: DebugCommand -> DebugCommand -> [DebugCommand]

enumFromTo :: DebugCommand -> DebugCommand -> [DebugCommand]

enumFromThenTo :: DebugCommand -> DebugCommand -> DebugCommand -> [DebugCommand]

Read DebugCommand

Defined in Cornelis.Types

Methods

readsPrec :: Int -> ReadS DebugCommand

readList :: ReadS [DebugCommand]

readPrec :: ReadPrec DebugCommand

readListPrec :: ReadPrec [DebugCommand]

Show DebugCommand

Defined in Cornelis.Types

Methods

showsPrec :: Int -> DebugCommand -> ShowS

show :: DebugCommand -> String

showList :: [DebugCommand] -> ShowS

Eq DebugCommand

Defined in Cornelis.Types

Methods

(==) :: DebugCommand -> DebugCommand -> Bool

(/=) :: DebugCommand -> DebugCommand -> Bool

Ord DebugCommand

Defined in Cornelis.Types

Methods

compare :: DebugCommand -> DebugCommand -> Ordering

(<) :: DebugCommand -> DebugCommand -> Bool

(<=) :: DebugCommand -> DebugCommand -> Bool

(>) :: DebugCommand -> DebugCommand -> Bool

(>=) :: DebugCommand -> DebugCommand -> Bool

max :: DebugCommand -> DebugCommand -> DebugCommand

min :: DebugCommand -> DebugCommand -> DebugCommand

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

Instances

FromJSON InteractionId

Defined in Cornelis.Types.Agda

Methods

parseJSON :: Value -> Parser InteractionId

parseJSONList :: Value -> Parser [InteractionId]

omittedField :: Maybe InteractionId

ToJSON InteractionId

Defined in Cornelis.Types.Agda

Methods

toJSON :: InteractionId -> Value

toEncoding :: InteractionId -> Encoding

toJSONList :: [InteractionId] -> Value

toEncodingList :: [InteractionId] -> Encoding

omitField :: InteractionId -> Bool

Enum InteractionId

Defined in Cornelis.Types.Agda

Methods

succ :: InteractionId -> InteractionId

pred :: InteractionId -> InteractionId

toEnum :: Int -> InteractionId

fromEnum :: InteractionId -> Int

enumFrom :: InteractionId -> [InteractionId]

enumFromThen :: InteractionId -> InteractionId -> [InteractionId]

enumFromTo :: InteractionId -> InteractionId -> [InteractionId]

enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]

Num InteractionId

Defined in Cornelis.Types.Agda

Methods

(+) :: InteractionId -> InteractionId -> InteractionId

(-) :: InteractionId -> InteractionId -> InteractionId

(*) :: InteractionId -> InteractionId -> InteractionId

negate :: InteractionId -> InteractionId

abs :: InteractionId -> InteractionId

signum :: InteractionId -> InteractionId

fromInteger :: Integer -> InteractionId

Read InteractionId

Defined in Cornelis.Types.Agda

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Integral InteractionId

Defined in Cornelis.Types.Agda

Methods

quot :: InteractionId -> InteractionId -> InteractionId

rem :: InteractionId -> InteractionId -> InteractionId

div :: InteractionId -> InteractionId -> InteractionId

mod :: InteractionId -> InteractionId -> InteractionId

quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)

toInteger :: InteractionId -> Integer

Real InteractionId

Defined in Cornelis.Types.Agda

Methods

toRational :: InteractionId -> Rational

Show InteractionId

Defined in Cornelis.Types.Agda

Methods

showsPrec :: Int -> InteractionId -> ShowS

show :: InteractionId -> String

showList :: [InteractionId] -> ShowS

Eq InteractionId

Defined in Cornelis.Types.Agda

Methods

(==) :: InteractionId -> InteractionId -> Bool

(/=) :: InteractionId -> InteractionId -> Bool

Ord InteractionId

Defined in Cornelis.Types.Agda

Methods

compare :: InteractionId -> InteractionId -> Ordering

(<) :: InteractionId -> InteractionId -> Bool

(<=) :: InteractionId -> InteractionId -> Bool

(>) :: InteractionId -> InteractionId -> Bool

(>=) :: InteractionId -> InteractionId -> Bool

max :: InteractionId -> InteractionId -> InteractionId

min :: InteractionId -> InteractionId -> InteractionId

data Buffer

Instances

Generic Buffer

Defined in Neovim.API.Text

Associated Types

type Rep Buffer :: Type -> Type

Methods

from :: Buffer -> Rep Buffer x

to :: Rep Buffer x -> Buffer

Show Buffer

Defined in Neovim.API.Text

Methods

showsPrec :: Int -> Buffer -> ShowS

show :: Buffer -> String

showList :: [Buffer] -> ShowS

NFData Buffer

Defined in Neovim.API.Text

Methods

rnf :: Buffer -> ()

Eq Buffer

Defined in Neovim.API.Text

Methods

(==) :: Buffer -> Buffer -> Bool

(/=) :: Buffer -> Buffer -> Bool

Ord Buffer

Defined in Cornelis.Types

Methods

compare :: Buffer -> Buffer -> Ordering

(<) :: Buffer -> Buffer -> Bool

(<=) :: Buffer -> Buffer -> Bool

(>) :: Buffer -> Buffer -> Bool

(>=) :: Buffer -> Buffer -> Bool

max :: Buffer -> Buffer -> Buffer

min :: Buffer -> Buffer -> Buffer

NvimObject Buffer

Defined in Neovim.API.Text

Methods

toObject :: Buffer -> Object

fromObjectUnsafe :: Object -> Buffer

fromObject :: Object -> Either (Doc AnsiStyle) Buffer

fromObject' :: MonadIO io => Object -> io 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)))

data Window

Instances

Generic Window

Defined in Neovim.API.Text

Associated Types

type Rep Window :: Type -> Type

Methods

from :: Window -> Rep Window x

to :: Rep Window x -> Window

Show Window

Defined in Neovim.API.Text

Methods

showsPrec :: Int -> Window -> ShowS

show :: Window -> String

showList :: [Window] -> ShowS

NFData Window

Defined in Neovim.API.Text

Methods

rnf :: Window -> ()

Eq Window

Defined in Neovim.API.Text

Methods

(==) :: Window -> Window -> Bool

(/=) :: Window -> Window -> Bool

NvimObject Window

Defined in Neovim.API.Text

Methods

toObject :: Window -> Object

fromObjectUnsafe :: Object -> Window

fromObject :: Object -> Either (Doc AnsiStyle) Window

fromObject' :: MonadIO io => Object -> io 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)))

data Text

A space efficient, packed, unboxed Unicode text type.

Instances

FromJSON Text

Defined in Data.Aeson.Types.FromJSON

Methods

parseJSON :: Value -> Parser Text

parseJSONList :: Value -> Parser [Text]

omittedField :: Maybe Text

FromJSONKey Text

Defined in Data.Aeson.Types.FromJSON

Methods

fromJSONKey :: FromJSONKeyFunction Text

fromJSONKeyList :: FromJSONKeyFunction [Text]

ToJSON Text

Defined in Data.Aeson.Types.ToJSON

Methods

toJSON :: Text -> Value

toEncoding :: Text -> Encoding

toJSONList :: [Text] -> Value

toEncodingList :: [Text] -> Encoding

omitField :: Text -> Bool

ToJSONKey Text

Defined in Data.Aeson.Types.ToJSON

Methods

toJSONKey :: ToJSONKeyFunction Text

toJSONKeyList :: ToJSONKeyFunction [Text]

Hashable Text

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> Text -> Int

hash :: Text -> Int

Ixed Text

Defined in Control.Lens.At

Methods

ix :: Index Text -> Traversal' Text (IxValue Text)

AsEmpty Text

Defined in Control.Lens.Empty

Methods

_Empty :: Prism' Text ()

Reversing Text

Defined in Control.Lens.Internal.Iso

Methods

reversing :: Text -> Text

Prefixed Text

Defined in Control.Lens.Prism

Methods

prefixed :: Text -> Prism' Text Text

Suffixed Text

Defined in Control.Lens.Prism

Methods

suffixed :: Text -> Prism' Text Text

Stream Text

Defined in Text.Megaparsec.Stream

Associated Types

type Token Text

type Tokens Text

Methods

tokenToChunk :: Proxy Text -> Token Text -> Tokens Text

tokensToChunk :: Proxy Text -> [Token Text] -> Tokens Text

chunkToTokens :: Proxy Text -> Tokens Text -> [Token Text]

chunkLength :: Proxy Text -> Tokens Text -> Int

chunkEmpty :: Proxy Text -> Tokens Text -> Bool

take1_ :: Text -> Maybe (Token Text, Text)

takeN_ :: Int -> Text -> Maybe (Tokens Text, Text)

takeWhile_ :: (Token Text -> Bool) -> Text -> (Tokens Text, Text)

TraversableStream Text

Defined in Text.Megaparsec.Stream

Methods

reachOffset :: Int -> PosState Text -> (Maybe String, PosState Text)

reachOffsetNoLine :: Int -> PosState Text -> PosState Text

VisualStream Text

Defined in Text.Megaparsec.Stream

Methods

showTokens :: Proxy Text -> NonEmpty (Token Text) -> String

tokensLength :: Proxy Text -> NonEmpty (Token Text) -> Int

GrowingAppend Text

Defined in Data.MonoTraversable

MonoFoldable Text

Defined in Data.MonoTraversable

Methods

ofoldMap :: Monoid m => (Element Text -> m) -> Text -> m

ofoldr :: (Element Text -> b -> b) -> b -> Text -> b

ofoldl' :: (a -> Element Text -> a) -> a -> Text -> a

otoList :: Text -> [Element Text]

oall :: (Element Text -> Bool) -> Text -> Bool

oany :: (Element Text -> Bool) -> Text -> Bool

onull :: Text -> Bool

olength :: Text -> Int

olength64 :: Text -> Int64

ocompareLength :: Integral i => Text -> i -> Ordering

otraverse_ :: Applicative f => (Element Text -> f b) -> Text -> f ()

ofor_ :: Applicative f => Text -> (Element Text -> f b) -> f ()

omapM_ :: Applicative m => (Element Text -> m ()) -> Text -> m ()

oforM_ :: Applicative m => Text -> (Element Text -> m ()) -> m ()

ofoldlM :: Monad m => (a -> Element Text -> m a) -> a -> Text -> m a

ofoldMap1Ex :: Semigroup m => (Element Text -> m) -> Text -> m

ofoldr1Ex :: (Element Text -> Element Text -> Element Text) -> Text -> Element Text

ofoldl1Ex' :: (Element Text -> Element Text -> Element Text) -> Text -> Element Text

headEx :: Text -> Element Text

lastEx :: Text -> Element Text

unsafeHead :: Text -> Element Text

unsafeLast :: Text -> Element Text

maximumByEx :: (Element Text -> Element Text -> Ordering) -> Text -> Element Text

minimumByEx :: (Element Text -> Element Text -> Ordering) -> Text -> Element Text

oelem :: Element Text -> Text -> Bool

onotElem :: Element Text -> Text -> Bool

MonoFunctor Text

Defined in Data.MonoTraversable

Methods

omap :: (Element Text -> Element Text) -> Text -> Text

MonoPointed Text

Defined in Data.MonoTraversable

Methods

opoint :: Element Text -> Text

MonoTraversable Text

Defined in Data.MonoTraversable

Methods

otraverse :: Applicative f => (Element Text -> f (Element Text)) -> Text -> f Text

omapM :: Applicative m => (Element Text -> m (Element Text)) -> Text -> m Text

IsSequence Text

Defined in Data.Sequences

Methods

fromList :: [Element Text] -> Text

lengthIndex :: Text -> Index Text

break :: (Element Text -> Bool) -> Text -> (Text, Text)

span :: (Element Text -> Bool) -> Text -> (Text, Text)

dropWhile :: (Element Text -> Bool) -> Text -> Text

takeWhile :: (Element Text -> Bool) -> Text -> Text

splitAt :: Index Text -> Text -> (Text, Text)

unsafeSplitAt :: Index Text -> Text -> (Text, Text)

take :: Index Text -> Text -> Text

unsafeTake :: Index Text -> Text -> Text

drop :: Index Text -> Text -> Text

unsafeDrop :: Index Text -> Text -> Text

dropEnd :: Index Text -> Text -> Text

partition :: (Element Text -> Bool) -> Text -> (Text, Text)

uncons :: Text -> Maybe (Element Text, Text)

unsnoc :: Text -> Maybe (Text, Element Text)

filter :: (Element Text -> Bool) -> Text -> Text

filterM :: Monad m => (Element Text -> m Bool) -> Text -> m Text

replicate :: Index Text -> Element Text -> Text

replicateM :: Monad m => Index Text -> m (Element Text) -> m Text

groupBy :: (Element Text -> Element Text -> Bool) -> Text -> [Text]

groupAllOn :: Eq b => (Element Text -> b) -> Text -> [Text]

subsequences :: Text -> [Text]

permutations :: Text -> [Text]

tailEx :: Text -> Text

tailMay :: Text -> Maybe Text

initEx :: Text -> Text

initMay :: Text -> Maybe Text

unsafeTail :: Text -> Text

unsafeInit :: Text -> Text

index :: Text -> Index Text -> Maybe (Element Text)

indexEx :: Text -> Index Text -> Element Text

unsafeIndex :: Text -> Index Text -> Element Text

splitWhen :: (Element Text -> Bool) -> Text -> [Text]

tails :: Text -> [Text]

inits :: Text -> [Text]

initTails :: Text -> [(Text, Text)]

SemiSequence Text

Defined in Data.Sequences

Associated Types

type Index Text

Methods

intersperse :: Element Text -> Text -> Text

reverse :: Text -> Text

find :: (Element Text -> Bool) -> Text -> Maybe (Element Text)

sortBy :: (Element Text -> Element Text -> Ordering) -> Text -> Text

cons :: Element Text -> Text -> Text

snoc :: Text -> Element Text -> Text

Textual Text

Defined in Data.Sequences

Methods

words :: Text -> [Text]

unwords :: (Element seq ~ Text, MonoFoldable seq) => seq -> Text

lines :: Text -> [Text]

unlines :: (Element seq ~ Text, MonoFoldable seq) => seq -> Text

toLower :: Text -> Text

toUpper :: Text -> Text

toCaseFold :: Text -> Text

breakWord :: Text -> (Text, Text)

breakLine :: Text -> (Text, Text)

NvimObject Text

Defined in Neovim.Classes

Methods

toObject :: Text -> Object

fromObjectUnsafe :: Object -> Text

fromObject :: Object -> Either (Doc AnsiStyle) Text

fromObject' :: MonadIO io => Object -> io Text

Pretty Text

Automatically converts all newlines to line.

>>> pretty ("hello\nworld" :: Text)
hello
world

Note that line can be undone by group:

>>> group (pretty ("hello\nworld" :: Text))
hello world

Manually use hardline if you definitely want newlines.

Defined in Prettyprinter.Internal

Methods

pretty :: Text -> Doc ann

prettyList :: [Text] -> Doc ann

LazySequence Text Text

Defined in Data.Sequences

Methods

toChunks :: Text -> [Text0]

fromChunks :: [Text0] -> Text

toStrict :: Text -> Text0

fromStrict :: Text0 -> Text

Utf8 Text ByteString

Defined in Data.Sequences

Methods

encodeUtf8 :: Text -> ByteString

decodeUtf8 :: ByteString -> Text

Cons Text Text Char Char

Defined in Control.Lens.Cons

Methods

_Cons :: Prism Text Text (Char, Text) (Char, Text)

Snoc Text Text Char Char

Defined in Control.Lens.Cons

Methods

_Snoc :: Prism Text Text (Text, Char) (Text, Char)

(a ~ Char, b ~ Char) => Each Text Text a b

each :: Traversal Text Text Char Char

Defined in Control.Lens.Each

Methods

each :: Traversal Text Text a b

Stream (NoShareInput Text)

Defined in Text.Megaparsec.Stream

Associated Types

type Token (NoShareInput Text)

type Tokens (NoShareInput Text)

Methods

tokenToChunk :: Proxy (NoShareInput Text) -> Token (NoShareInput Text) -> Tokens (NoShareInput Text)

tokensToChunk :: Proxy (NoShareInput Text) -> [Token (NoShareInput Text)] -> Tokens (NoShareInput Text)

chunkToTokens :: Proxy (NoShareInput Text) -> Tokens (NoShareInput Text) -> [Token (NoShareInput Text)]

chunkLength :: Proxy (NoShareInput Text) -> Tokens (NoShareInput Text) -> Int

chunkEmpty :: Proxy (NoShareInput Text) -> Tokens (NoShareInput Text) -> Bool

take1_ :: NoShareInput Text -> Maybe (Token (NoShareInput Text), NoShareInput Text)

takeN_ :: Int -> NoShareInput Text -> Maybe (Tokens (NoShareInput Text), NoShareInput Text)

takeWhile_ :: (Token (NoShareInput Text) -> Bool) -> NoShareInput Text -> (Tokens (NoShareInput Text), NoShareInput Text)

Stream (ShareInput Text)

Defined in Text.Megaparsec.Stream

Associated Types

type Token (ShareInput Text)

type Tokens (ShareInput Text)

Methods

tokenToChunk :: Proxy (ShareInput Text) -> Token (ShareInput Text) -> Tokens (ShareInput Text)

tokensToChunk :: Proxy (ShareInput Text) -> [Token (ShareInput Text)] -> Tokens (ShareInput Text)

chunkToTokens :: Proxy (ShareInput Text) -> Tokens (ShareInput Text) -> [Token (ShareInput Text)]

chunkLength :: Proxy (ShareInput Text) -> Tokens (ShareInput Text) -> Int

chunkEmpty :: Proxy (ShareInput Text) -> Tokens (ShareInput Text) -> Bool

take1_ :: ShareInput Text -> Maybe (Token (ShareInput Text), ShareInput Text)

takeN_ :: Int -> ShareInput Text -> Maybe (Tokens (ShareInput Text), ShareInput Text)

takeWhile_ :: (Token (ShareInput Text) -> Bool) -> ShareInput Text -> (Tokens (ShareInput Text), ShareInput Text)

type Item Text

Defined in Data.Text

type Item Text = Char

type Index Text

Defined in Control.Lens.At

type Index Text = Int

type IxValue Text

Defined in Control.Lens.At

type IxValue Text = Char

type Token Text

Defined in Text.Megaparsec.Stream

type Token Text = Token (ShareInput Text)

type Tokens Text

Defined in Text.Megaparsec.Stream

type Tokens Text = Tokens (ShareInput Text)

type Element Text

Defined in Data.MonoTraversable

type Element Text = Char

type Index Text

Defined in Data.Sequences

type Index Text = Int

type Token (NoShareInput Text)

Defined in Text.Megaparsec.Stream

type Token (NoShareInput Text) = Char

type Token (ShareInput Text)

Defined in Text.Megaparsec.Stream

type Token (ShareInput Text) = Char

type Tokens (NoShareInput Text)

Defined in Text.Megaparsec.Stream

type Tokens (NoShareInput Text) = Text

type Tokens (ShareInput Text)

Defined in Text.Megaparsec.Stream

type Tokens (ShareInput Text) = Text

traceMX :: Show a => String -> a -> Neovim env ()

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

Methods

parseJSON :: Value -> Parser AgdaInterval

parseJSONList :: Value -> Parser [AgdaInterval]

omittedField :: Maybe AgdaInterval

Ord Buffer

Methods

compare :: Buffer -> Buffer -> Ordering

(<) :: Buffer -> Buffer -> Bool

(<=) :: Buffer -> Buffer -> Bool

(>) :: Buffer -> Buffer -> Bool

(>=) :: Buffer -> Buffer -> Bool

max :: Buffer -> Buffer -> Buffer

min :: Buffer -> Buffer -> Buffer