-
Notifications
You must be signed in to change notification settings - Fork 18
Open
Description
The current TH-based design makes a lot of usual Haskellisms rather annoying, eg, requiring an explicit binding to get a function into the right shape
doRefine :: CommandArguments -> Neovim CornelisEnv ()
doRefine = const refine
refine :: Neovim CornelisEnv ()
refine = withAgda $ void $ withGoalAtCursor $ \b goal -> do
agda <- getAgda b
flip runIOTCM agda $ Cmd_refine_or_intro True (InteractionId $ ip_id goal) noRange ""
just to export it:
$(command "CornelisRefine" 'doRefine) [CmdSync Async]
For simple cases like this, it would be nice to have a function:
exportCommand :: String -> (CommandArguments -> Neovim env ()) -> [CommandOption] -> ExportedFunctionality env
such that the above call could be implemented more simply as
exportCommand "CornelisRefine" (const refine) [CmdSync Async]
which avoids the TH and prevents needing to define the no-op doRefine
.
Metadata
Metadata
Assignees
Labels
No labels