{-# LANGUAGE NumDecimals #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Lib where
import Control.Arrow ((&&&))
import Control.Concurrent.Chan.Unagi
import Control.Lens
import Control.Monad (forever, when)
import Control.Monad.State.Class (gets)
import Cornelis.Config (getConfig)
import Cornelis.Debug (reportExceptions)
import Cornelis.Goals
import Cornelis.Highlighting (highlightBuffer, getLineIntervals, lookupPoint)
import Cornelis.InfoWin
import Cornelis.Offsets
import Cornelis.Subscripts (incNextDigitSeq, decNextDigitSeq)
import Cornelis.Types
import Cornelis.Utils
import Cornelis.Vim
import Data.Foldable (for_)
import Data.IORef (newIORef)
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Text as T
import Neovim
import Neovim.API.Text
import Neovim.Plugin (CommandOption(CmdComplete))
import Plugin
getInteractionPoint
:: Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint :: Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i = (CornelisState -> Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CornelisState -> Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity)))
-> (CornelisState -> Maybe (InteractionPoint Identity))
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
forall a b. (a -> b) -> a -> b
$ Getting
(First (InteractionPoint Identity))
CornelisState
(InteractionPoint Identity)
-> CornelisState -> Maybe (InteractionPoint Identity)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview (Getting
(First (InteractionPoint Identity))
CornelisState
(InteractionPoint Identity)
-> CornelisState -> Maybe (InteractionPoint Identity))
-> Getting
(First (InteractionPoint Identity))
CornelisState
(InteractionPoint Identity)
-> CornelisState
-> Maybe (InteractionPoint Identity)
forall a b. (a -> b) -> a -> b
$ (Map Buffer BufferStuff
-> Const
(First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> CornelisState
-> Const (First (InteractionPoint Identity)) CornelisState
#cs_buffers ((Map Buffer BufferStuff
-> Const
(First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> CornelisState
-> Const (First (InteractionPoint Identity)) CornelisState)
-> ((InteractionPoint Identity
-> Const
(First (InteractionPoint Identity)) (InteractionPoint Identity))
-> Map Buffer BufferStuff
-> Const
(First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> Getting
(First (InteractionPoint Identity))
CornelisState
(InteractionPoint Identity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Buffer BufferStuff)
-> Traversal'
(Map Buffer BufferStuff) (IxValue (Map Buffer BufferStuff))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map Buffer BufferStuff)
Buffer
b ((IxValue (Map Buffer BufferStuff)
-> Const
(First (InteractionPoint Identity))
(IxValue (Map Buffer BufferStuff)))
-> Map Buffer BufferStuff
-> Const
(First (InteractionPoint Identity)) (Map Buffer BufferStuff))
-> ((InteractionPoint Identity
-> Const
(First (InteractionPoint Identity)) (InteractionPoint Identity))
-> IxValue (Map Buffer BufferStuff)
-> Const
(First (InteractionPoint Identity))
(IxValue (Map Buffer BufferStuff)))
-> (InteractionPoint Identity
-> Const
(First (InteractionPoint Identity)) (InteractionPoint Identity))
-> Map Buffer BufferStuff
-> Const
(First (InteractionPoint Identity)) (Map Buffer BufferStuff)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map InteractionId (InteractionPoint Identity)
-> Const
(First (InteractionPoint Identity))
(Map InteractionId (InteractionPoint Identity)))
-> IxValue (Map Buffer BufferStuff)
-> Const
(First (InteractionPoint Identity))
(IxValue (Map Buffer BufferStuff))
#bs_ips ((Map InteractionId (InteractionPoint Identity)
-> Const
(First (InteractionPoint Identity))
(Map InteractionId (InteractionPoint Identity)))
-> IxValue (Map Buffer BufferStuff)
-> Const
(First (InteractionPoint Identity))
(IxValue (Map Buffer BufferStuff)))
-> ((InteractionPoint Identity
-> Const
(First (InteractionPoint Identity)) (InteractionPoint Identity))
-> Map InteractionId (InteractionPoint Identity)
-> Const
(First (InteractionPoint Identity))
(Map InteractionId (InteractionPoint Identity)))
-> (InteractionPoint Identity
-> Const
(First (InteractionPoint Identity)) (InteractionPoint Identity))
-> IxValue (Map Buffer BufferStuff)
-> Const
(First (InteractionPoint Identity))
(IxValue (Map Buffer BufferStuff))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map InteractionId (InteractionPoint Identity))
-> Traversal'
(Map InteractionId (InteractionPoint Identity))
(IxValue (Map InteractionId (InteractionPoint Identity)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map InteractionId (InteractionPoint Identity))
InteractionId
i
respondToHelperFunction :: DisplayInfo -> Neovim env ()
respondToHelperFunction :: forall env. DisplayInfo -> Neovim env ()
respondToHelperFunction (HelperFunction Text
sig) = Text -> Text -> Neovim env ()
forall env. Text -> Text -> Neovim env ()
setreg Text
"\"" Text
sig
respondToHelperFunction DisplayInfo
_ = () -> Neovim env ()
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
respond :: Buffer -> Response -> Neovim CornelisEnv ()
respond :: Buffer -> Response -> Neovim CornelisEnv ()
respond Buffer
b (DisplayInfo DisplayInfo
dp) = do
DisplayInfo -> Neovim CornelisEnv ()
forall env. DisplayInfo -> Neovim env ()
respondToHelperFunction DisplayInfo
dp
Bool -> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DisplayInfo
dp DisplayInfo -> (DisplayInfo -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
& Getting
All
DisplayInfo
(InteractionPoint Identity, [InScope], Type, Maybe Type,
Maybe [Text], Maybe [Text])
-> DisplayInfo -> Bool
forall s a. Getting All s a -> s -> Bool
hasn't Getting
All
DisplayInfo
(InteractionPoint Identity, [InScope], Type, Maybe Type,
Maybe [Text], Maybe [Text])
#_GoalSpecific) (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$
Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter BufferStuff BufferStuff DisplayInfo DisplayInfo
#bs_goals ASetter BufferStuff BufferStuff DisplayInfo DisplayInfo
-> DisplayInfo -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ DisplayInfo
dp
Buffer -> DisplayInfo -> Neovim CornelisEnv ()
goalWindow Buffer
b DisplayInfo
dp
respond Buffer
b (InteractionPoints [InteractionPoint Maybe]
ips) = do
let ips' :: [InteractionPoint Identity]
ips' = (InteractionPoint Maybe -> Maybe (InteractionPoint Identity))
-> [InteractionPoint Maybe] -> [InteractionPoint Identity]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe InteractionPoint Maybe -> Maybe (InteractionPoint Identity)
forall (f :: * -> *).
Applicative f =>
InteractionPoint f -> f (InteractionPoint Identity)
sequenceInteractionPoint [InteractionPoint Maybe]
ips
Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ ASetter
BufferStuff
BufferStuff
(Map InteractionId (InteractionPoint Identity))
(Map InteractionId (InteractionPoint Identity))
#bs_ips ASetter
BufferStuff
BufferStuff
(Map InteractionId (InteractionPoint Identity))
(Map InteractionId (InteractionPoint Identity))
-> Map InteractionId (InteractionPoint Identity)
-> BufferStuff
-> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [(InteractionId, InteractionPoint Identity)]
-> Map InteractionId (InteractionPoint Identity)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((InteractionPoint Identity
-> (InteractionId, InteractionPoint Identity))
-> [InteractionPoint Identity]
-> [(InteractionId, InteractionPoint Identity)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id (InteractionPoint Identity -> InteractionId)
-> (InteractionPoint Identity -> InteractionPoint Identity)
-> InteractionPoint Identity
-> (InteractionId, InteractionPoint Identity)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& InteractionPoint Identity -> InteractionPoint Identity
forall a. a -> a
id) [InteractionPoint Identity]
ips')
respond Buffer
b (MakeCase MakeCase
mkcase) = do
Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase Buffer
b MakeCase
mkcase
Neovim CornelisEnv ()
load
respond Buffer
b (GiveAction Text
result InteractionPoint (Const ())
ip) = do
let i :: InteractionId
i = InteractionPoint (Const ()) -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id InteractionPoint (Const ())
ip
Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> (Maybe (InteractionPoint Identity) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv ()
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (InteractionPoint Identity)
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"Can't find interaction point " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> InteractionId -> String
forall a. Show a => a -> String
show InteractionId
i
Just InteractionPoint Identity
ip' -> do
AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip'
Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceQuestion Text
result
Neovim CornelisEnv ()
load
respond Buffer
b (SolveAll [Solution]
solutions) = do
[Solution]
-> (Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Solution]
solutions ((Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Solution -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \(Solution InteractionId
i Text
ex) ->
Buffer
-> InteractionId
-> Neovim CornelisEnv (Maybe (InteractionPoint Identity))
getInteractionPoint Buffer
b InteractionId
i Neovim CornelisEnv (Maybe (InteractionPoint Identity))
-> (Maybe (InteractionPoint Identity) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv ()
forall a b.
Neovim CornelisEnv a
-> (a -> Neovim CornelisEnv b) -> Neovim CornelisEnv b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (InteractionPoint Identity)
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"Can't find interaction point " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> InteractionId -> String
forall a. Show a => a -> String
show InteractionId
i
Just InteractionPoint Identity
ip -> do
AgdaInterval
int <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int (Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceQuestion Text
ex
Neovim CornelisEnv ()
load
respond Buffer
b Response
ClearHighlighting = do
Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> BufferStuff
bs
BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
BufferStuff
BufferStuff
(Map Extmark DefinitionSite)
(Map Extmark DefinitionSite)
#bs_goto_sites ASetter
BufferStuff
BufferStuff
(Map Extmark DefinitionSite)
(Map Extmark DefinitionSite)
-> Map Extmark DefinitionSite -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map Extmark DefinitionSite
forall a. Monoid a => a
mempty
BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
BufferStuff
BufferStuff
(Map InteractionId Extmark)
(Map InteractionId Extmark)
#bs_ip_exts ASetter
BufferStuff
BufferStuff
(Map InteractionId Extmark)
(Map InteractionId Extmark)
-> Map InteractionId Extmark -> BufferStuff -> BufferStuff
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map InteractionId Extmark
forall a. Monoid a => a
mempty
Int64
ns <- (CornelisEnv -> Int64) -> Neovim CornelisEnv Int64
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CornelisEnv -> Int64
ce_namespace
Buffer -> Int64 -> Int64 -> Int64 -> Neovim CornelisEnv ()
forall env. Buffer -> Int64 -> Int64 -> Int64 -> Neovim env ()
nvim_buf_clear_namespace Buffer
b Int64
ns Int64
0 (-Int64
1)
respond Buffer
b (HighlightingInfo Bool
_remove [Highlight]
hl) = do
Map AgdaInterval Extmark
extmap <- Buffer
-> [Highlight] -> Neovim CornelisEnv (Map AgdaInterval Extmark)
highlightBuffer Buffer
b [Highlight]
hl
Buffer -> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
modifyBufferStuff Buffer
b ((BufferStuff -> BufferStuff) -> Neovim CornelisEnv ())
-> (BufferStuff -> BufferStuff) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ \BufferStuff
bs -> BufferStuff
bs
BufferStuff -> (BufferStuff -> BufferStuff) -> BufferStuff
forall a b. a -> (a -> b) -> b
& ASetter
BufferStuff
BufferStuff
(Map InteractionId Extmark)
(Map InteractionId Extmark)
#bs_ip_exts ASetter
BufferStuff
BufferStuff
(Map InteractionId Extmark)
(Map InteractionId Extmark)
-> Map InteractionId Extmark -> BufferStuff -> BufferStuff
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Map AgdaInterval Extmark
-> Map InteractionId AgdaInterval -> Map InteractionId Extmark
forall b c a. Ord b => Map b c -> Map a b -> Map a c
M.compose Map AgdaInterval Extmark
extmap ((InteractionPoint Identity -> AgdaInterval)
-> Map InteractionId (InteractionPoint Identity)
-> Map InteractionId AgdaInterval
forall a b. (a -> b) -> Map InteractionId a -> Map InteractionId b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InteractionPoint Identity -> AgdaInterval
ip_interval' (Map InteractionId (InteractionPoint Identity)
-> Map InteractionId AgdaInterval)
-> Map InteractionId (InteractionPoint Identity)
-> Map InteractionId AgdaInterval
forall a b. (a -> b) -> a -> b
$ BufferStuff -> Map InteractionId (InteractionPoint Identity)
bs_ips BufferStuff
bs)
respond Buffer
_ (RunningInfo Int
_ Text
x) = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
x
respond Buffer
_ Response
ClearRunningInfo = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportInfo Text
""
respond Buffer
b (JumpToError String
_ Index 'CodePoint 'OneIndexed
pos) = do
Bool -> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a (e :: Unit). Num a => Index e 'OneIndexed -> a
fromOneIndexed @Int Index 'CodePoint 'OneIndexed
pos Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
50) (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
Vector Text
buf_lines <- Buffer
-> Int64 -> Int64 -> Bool -> Neovim CornelisEnv (Vector Text)
forall env.
Buffer -> Int64 -> Int64 -> Bool -> Neovim env (Vector Text)
nvim_buf_get_lines Buffer
b Int64
0 (-Int64
1) Bool
True
let li :: LineIntervals
li = Vector Text -> LineIntervals
getLineIntervals Vector Text
buf_lines
case LineIntervals -> Index 'CodePoint 'OneIndexed -> Maybe VimPos
lookupPoint LineIntervals
li Index 'CodePoint 'OneIndexed
pos of
Maybe VimPos
Nothing -> Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError Text
"invalid error report from Agda"
Just (Pos Index 'Line 'ZeroIndexed
l Index 'Byte 'ZeroIndexed
c) -> do
Maybe Window
ws <- ([Window] -> Maybe Window)
-> Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window)
forall a b.
(a -> b) -> Neovim CornelisEnv a -> Neovim CornelisEnv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Window] -> Maybe Window
forall a. [a] -> Maybe a
listToMaybe (Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window))
-> Neovim CornelisEnv [Window] -> Neovim CornelisEnv (Maybe Window)
forall a b. (a -> b) -> a -> b
$ Buffer -> Neovim CornelisEnv [Window]
forall env. Buffer -> Neovim env [Window]
windowsForBuffer Buffer
b
Maybe Window
-> (Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe Window
ws ((Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ())
-> (Window -> Neovim CornelisEnv ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ (Window -> (Int64, Int64) -> Neovim CornelisEnv ())
-> (Int64, Int64) -> Window -> Neovim CornelisEnv ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Window -> (Int64, Int64) -> Neovim CornelisEnv ()
forall env. Window -> (Int64, Int64) -> Neovim env ()
window_set_cursor (Index 'Line 'OneIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'OneIndexed -> a
fromOneIndexed (Index 'Line 'ZeroIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit). Index e 'ZeroIndexed -> Index e 'OneIndexed
oneIndex Index 'Line 'ZeroIndexed
l), Index 'Byte 'ZeroIndexed -> Int64
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed Index 'Byte 'ZeroIndexed
c)
respond Buffer
_ Status{} = () -> Neovim CornelisEnv ()
forall a. a -> Neovim CornelisEnv a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
respond Buffer
_ (Unknown Text
k Value
_) = Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError Text
k
{-# HLINT ignore doMakeCase "Functor law" #-}
doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
doMakeCase Buffer
b (RegularCase MakeCaseVariant
Function [Text]
clauses InteractionPoint Identity
ip) = do
AgdaInterval
int' <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
let int :: AgdaInterval
int = AgdaInterval
int' AgdaInterval -> (AgdaInterval -> AgdaInterval) -> AgdaInterval
forall a b. a -> (a -> b) -> b
& (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval
#iStart ((Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval)
-> ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval
-> Identity AgdaInterval
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval)
-> Index 'CodePoint 'OneIndexed -> AgdaInterval -> AgdaInterval
forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a (e :: Unit). Integral a => a -> Index e 'OneIndexed
toOneIndexed @Int Int
1
Int
ins <- Buffer -> Index 'Line 'ZeroIndexed -> Neovim CornelisEnv Int
forall env. Buffer -> Index 'Line 'ZeroIndexed -> Neovim env Int
getIndent Buffer
b (Index 'Line 'OneIndexed -> Index 'Line 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex (Pos 'CodePoint 'OneIndexed 'OneIndexed -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line (AgdaInterval -> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall p. Interval p -> p
iStart AgdaInterval
int)))
Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b AgdaInterval
int
(Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
T.replicate Int
ins Text
" " <>)
([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
replaceQuestion [Text]
clauses
doMakeCase Buffer
b (RegularCase MakeCaseVariant
ExtendedLambda [Text]
clauses InteractionPoint Identity
ip) = do
[Window]
ws <- Buffer -> Neovim CornelisEnv [Window]
forall env. Buffer -> Neovim env [Window]
windowsForBuffer Buffer
b
case [Window] -> Maybe Window
forall a. [a] -> Maybe a
listToMaybe [Window]
ws of
Maybe Window
Nothing ->
Text -> Neovim CornelisEnv ()
forall env. Text -> Neovim env ()
reportError
Text
"Unable to extend a lambda without having a window that contains the modified buffer. This is a limitation in cornelis."
Just Window
w -> do
AgdaInterval
int' <- Buffer
-> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval
getIpInterval Buffer
b InteractionPoint Identity
ip
Interval Pos 'CodePoint 'OneIndexed 'OneIndexed
start Pos 'CodePoint 'OneIndexed 'OneIndexed
end
<- Window -> Buffer -> AgdaInterval -> Neovim CornelisEnv AgdaInterval
forall env.
Window -> Buffer -> AgdaInterval -> Neovim env AgdaInterval
getLambdaClause Window
w Buffer
b (AgdaInterval
int' AgdaInterval -> (AgdaInterval -> AgdaInterval) -> AgdaInterval
forall a b. a -> (a -> b) -> b
& (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval
#iStart ((Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval)
-> ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval
-> Identity AgdaInterval
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> AgdaInterval -> Identity AgdaInterval)
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> AgdaInterval
-> AgdaInterval
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset (- Int
1)))
Buffer -> AgdaInterval -> Text -> Neovim CornelisEnv ()
forall env. Buffer -> AgdaInterval -> Text -> Neovim env ()
replaceInterval Buffer
b (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed -> AgdaInterval
forall p. p -> p -> Interval p
Interval (Pos 'CodePoint 'OneIndexed 'OneIndexed
start Pos 'CodePoint 'OneIndexed 'OneIndexed
-> (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall a b. a -> (a -> b) -> b
& (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset Int
1)) (Pos 'CodePoint 'OneIndexed 'OneIndexed
end Pos 'CodePoint 'OneIndexed 'OneIndexed
-> (Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall a b. a -> (a -> b) -> b
& (Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed)
#p_col ((Index 'CodePoint 'OneIndexed
-> Identity (Index 'CodePoint 'OneIndexed))
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Identity (Pos 'CodePoint 'OneIndexed 'OneIndexed))
-> (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'OneIndexed)
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
-> Pos 'CodePoint 'OneIndexed 'OneIndexed
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Index 'CodePoint 'OneIndexed
-> Offset 'CodePoint -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing).
Index e i -> Offset e -> Index e i
.+ Int -> Offset 'CodePoint
forall (e :: Unit). Int -> Offset e
Offset (- Int
2))))
(Text -> Neovim CornelisEnv ()) -> Text -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
replaceQuestion [Text]
clauses [Text] -> ([Text] -> [Text]) -> [Text]
forall a b. a -> (a -> b) -> b
& ([Text] -> Identity [Text]) -> [Text] -> Identity [Text]
forall s a. Cons s s a a => Traversal' s s
Traversal' [Text] [Text]
_tail (([Text] -> Identity [Text]) -> [Text] -> Identity [Text])
-> ([Text] -> [Text]) -> [Text] -> [Text]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pos 'CodePoint 'OneIndexed 'OneIndexed -> Text -> Text
indent Pos 'CodePoint 'OneIndexed 'OneIndexed
start)
indent :: AgdaPos -> Text -> Text
indent :: Pos 'CodePoint 'OneIndexed 'OneIndexed -> Text -> Text
indent (Pos Index 'Line 'OneIndexed
_ Index 'CodePoint 'OneIndexed
c) Text
s = [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
[ (Int -> Text -> Text) -> Text -> Int -> Text
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Text -> Text
T.replicate Text
" " (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Index 'CodePoint 'ZeroIndexed -> Int
forall a (e :: Unit). Num a => Index e 'ZeroIndexed -> a
fromZeroIndexed (Index 'CodePoint 'OneIndexed -> Index 'CodePoint 'ZeroIndexed
forall (e :: Unit). Index e 'OneIndexed -> Index e 'ZeroIndexed
zeroIndex Index 'CodePoint 'OneIndexed
c) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
, Text
"; "
, Text
s
]
doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()
doPrevGoal :: CommandArguments -> Neovim CornelisEnv ()
doPrevGoal = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
prevGoal
doNextGoal :: CommandArguments -> Neovim CornelisEnv ()
doNextGoal :: CommandArguments -> Neovim CornelisEnv ()
doNextGoal = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
nextGoal
doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doIncNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doIncNextDigitSeq = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
forall env. Neovim env ()
incNextDigitSeq
doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doDecNextDigitSeq :: CommandArguments -> Neovim CornelisEnv ()
doDecNextDigitSeq = Neovim CornelisEnv () -> CommandArguments -> Neovim CornelisEnv ()
forall a b. a -> b -> a
const Neovim CornelisEnv ()
forall env. Neovim env ()
decNextDigitSeq
cornelisInit :: Neovim env CornelisEnv
cornelisInit :: forall env. Neovim env CornelisEnv
cornelisInit = do
(InChan AgdaResp
inchan, OutChan AgdaResp
outchan) <- IO (InChan AgdaResp, OutChan AgdaResp)
-> Neovim env (InChan AgdaResp, OutChan AgdaResp)
forall a. IO a -> Neovim env a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (InChan AgdaResp, OutChan AgdaResp)
forall a. IO (InChan a, OutChan a)
newChan
Int64
ns <- Text -> Neovim env Int64
forall env. Text -> Neovim env Int64
nvim_create_namespace Text
"cornelis"
IORef CornelisState
mvar <- IO (IORef CornelisState) -> Neovim env (IORef CornelisState)
forall a. IO a -> Neovim env a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef CornelisState) -> Neovim env (IORef CornelisState))
-> IO (IORef CornelisState) -> Neovim env (IORef CornelisState)
forall a b. (a -> b) -> a -> b
$ CornelisState -> IO (IORef CornelisState)
forall a. a -> IO (IORef a)
newIORef (CornelisState -> IO (IORef CornelisState))
-> CornelisState -> IO (IORef CornelisState)
forall a b. (a -> b) -> a -> b
$ Map Buffer BufferStuff -> Map Int64 Diff0 -> CornelisState
CornelisState Map Buffer BufferStuff
forall a. Monoid a => a
mempty Map Int64 Diff0
forall a. Monoid a => a
mempty
CornelisConfig
cfg <- Neovim env CornelisConfig
forall env. Neovim env CornelisConfig
getConfig
let env :: CornelisEnv
env = IORef CornelisState
-> InChan AgdaResp -> Int64 -> CornelisConfig -> CornelisEnv
CornelisEnv IORef CornelisState
mvar InChan AgdaResp
inchan Int64
ns CornelisConfig
cfg
Neovim env (Async Any) -> Neovim env ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim env (Async Any) -> Neovim env ())
-> Neovim env (Async Any) -> Neovim env ()
forall a b. (a -> b) -> a -> b
$ CornelisEnv
-> Neovim CornelisEnv (Async Any) -> Neovim env (Async Any)
forall env a env'. env -> Neovim env a -> Neovim env' a
withLocalEnv CornelisEnv
env (Neovim CornelisEnv (Async Any) -> Neovim env (Async Any))
-> Neovim CornelisEnv (Async Any) -> Neovim env (Async Any)
forall a b. (a -> b) -> a -> b
$
Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any))
-> Neovim CornelisEnv Any -> Neovim CornelisEnv (Async Any)
forall a b. (a -> b) -> a -> b
$ do
Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (Neovim CornelisEnv () -> Neovim CornelisEnv Any)
-> Neovim CornelisEnv () -> Neovim CornelisEnv Any
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall env. Neovim env () -> Neovim env ()
reportExceptions (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ do
AgdaResp Buffer
buffer Response
next <- IO AgdaResp -> Neovim CornelisEnv AgdaResp
forall a. IO a -> Neovim CornelisEnv a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AgdaResp -> Neovim CornelisEnv AgdaResp)
-> IO AgdaResp -> Neovim CornelisEnv AgdaResp
forall a b. (a -> b) -> a -> b
$ OutChan AgdaResp -> IO AgdaResp
forall a. OutChan a -> IO a
readChan OutChan AgdaResp
outchan
Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ())
-> Neovim CornelisEnv (Async ()) -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv (Async ())
forall (m :: * -> *) a. MonadUnliftIO m => m a -> m (Async a)
neovimAsync (Neovim CornelisEnv () -> Neovim CornelisEnv (Async ()))
-> Neovim CornelisEnv () -> Neovim CornelisEnv (Async ())
forall a b. (a -> b) -> a -> b
$ Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall env. Neovim env () -> Neovim env ()
reportExceptions (Neovim CornelisEnv () -> Neovim CornelisEnv ())
-> Neovim CornelisEnv () -> Neovim CornelisEnv ()
forall a b. (a -> b) -> a -> b
$ Buffer -> Response -> Neovim CornelisEnv ()
respond Buffer
buffer Response
next
CornelisEnv -> Neovim env CornelisEnv
forall a. a -> Neovim env a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CornelisEnv
env
$(pure [])
main :: IO ()
main :: IO ()
main = NeovimConfig -> IO ()
neovim NeovimConfig
defaultConfig { plugins = [cornelis] }
cornelis :: Neovim () NeovimPlugin
cornelis :: Neovim () NeovimPlugin
cornelis = do
CornelisEnv
env <- Neovim () CornelisEnv
forall env. Neovim env CornelisEnv
cornelisInit
Neovim () ()
forall env. Neovim env ()
closeInfoWindows
let rw_complete :: CommandOption
rw_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisRewriteModeCompletion"
cm_complete :: CommandOption
cm_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisComputeModeCompletion"
debug_complete :: CommandOption
debug_complete = String -> CommandOption
CmdComplete String
"custom,InternalCornelisDebugCommandCompletion"
Plugin CornelisEnv -> Neovim () NeovimPlugin
forall (m :: * -> *) env.
Applicative m =>
Plugin env -> m NeovimPlugin
wrapPlugin (Plugin CornelisEnv -> Neovim () NeovimPlugin)
-> Plugin CornelisEnv -> Neovim () NeovimPlugin
forall a b. (a -> b) -> a -> b
$ Plugin
{ environment :: CornelisEnv
environment = CornelisEnv
env
, exports :: [ExportedFunctionality CornelisEnv]
exports =
[ $(command "CornelisRestart" 'doRestart) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisAbort" 'doAbort) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisLoad" 'doLoad) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisGoals" 'doAllGoals) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisSolve" 'solveOne) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
, $(command "CornelisAuto" 'autoOne) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisTypeInfer" 'doTypeInfer) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisTypeContext" 'typeContext) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
, $(command "CornelisTypeContextInfer" 'typeContextInfer) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
, $(command "CornelisMakeCase" 'doCaseSplit) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisRefine" 'doRefine) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisGive" 'doGive) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisElaborate" 'doElaborate) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
, $(command "CornelisPrevGoal" 'doPrevGoal) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisNextGoal" 'doNextGoal) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisGoToDefinition" 'doGotoDefinition) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisWhyInScope" 'doWhyInScope) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisNormalize" 'doNormalize) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
cm_complete]
, $(command "CornelisHelperFunc" 'doHelperFunc) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
rw_complete]
, $(command "CornelisQuestionToMeta" 'doQuestionToMeta) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisInc" 'doIncNextDigitSeq) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisDec" 'doDecNextDigitSeq) [Synchronous -> CommandOption
CmdSync Synchronous
Async]
, $(command "CornelisDebug" 'doDebug) [Synchronous -> CommandOption
CmdSync Synchronous
Async, CommandOption
debug_complete]
, $(command "CornelisCloseInfoWindows" 'doCloseInfoWindows) [Synchronous -> CommandOption
CmdSync Synchronous
Sync]
, $(function "InternalCornelisRewriteModeCompletion" 'rewriteModeCompletion) Synchronous
Sync
, $(function "InternalCornelisComputeModeCompletion" 'computeModeCompletion) Synchronous
Sync
, $(function "InternalCornelisDebugCommandCompletion" 'debugCommandCompletion) Synchronous
Sync
, $(function "InternalCornelisNotifyEdit" 'notifyEdit) Synchronous
Async
]
}