Get Agda version via interaction mode

Author: phijor

src/Cornelis/Types.hs

@@ -317,6 +317,7 @@ data DisplayInfo
   | IntroConstructorUnknown [Text]
   | WhyInScope Text
   | NormalForm Text
+  | Version Text
   | UnknownDisplayInfo Value
   deriving (Eq, Ord, Show, Generic)
 
@@ -365,6 +366,7 @@ instance FromJSON DisplayInfo where
               InferredType <$> info .: "expr"
             (_ :: Text) ->
               pure $ UnknownDisplayInfo v
+      "Version" -> Version <$> obj .: "version"
       (_ :: Text) -> pure $ UnknownDisplayInfo v
 
 instance FromJSON Response where

src/Lib.hs

@@ -42,6 +42,7 @@ getInteractionPoint b i = gets $ preview $ #cs_buffers . ix b . #bs_ips . ix i
 
 respondToHelperFunction :: DisplayInfo -> Neovim env ()
 respondToHelperFunction (HelperFunction sig) = setreg "\"" sig
+respondToHelperFunction (Version ver) = reportInfo ver
 respondToHelperFunction _ = pure ()
 
 
@@ -222,6 +223,7 @@ cornelis = do
         , $(command "CornelisQuestionToMeta"   'doQuestionToMeta)   [CmdSync Async]
         , $(command "CornelisInc"              'doIncNextDigitSeq)  [CmdSync Async]
         , $(command "CornelisDec"              'doDecNextDigitSeq)  [CmdSync Async]
+        , $(command "CornelisAgdaVersion"      'doGetVersion)       [CmdSync Async]
         , $(command "CornelisDebug"            'doDebug)            [CmdSync Async, debug_complete]
         , $(command "CornelisCloseInfoWindows" 'doCloseInfoWindows) [CmdSync Sync]
         , $(function "InternalCornelisRewriteModeCompletion" 'rewriteModeCompletion) Sync

src/Plugin.hs

@@ -330,6 +330,12 @@ caseSplit thing = withAgda $ void $ withGoalAtCursor $ \b ip -> do
         (mkAbsPathRnage fp $ ip_interval' ip)
     $ T.unpack thing
 
+getVersion :: Neovim CornelisEnv ()
+getVersion = withAgda $ void $ withCurrentBuffer $ getAgda >=> runIOTCM Cmd_show_version
+
+doGetVersion :: CommandArguments -> Neovim CornelisEnv ()
+doGetVersion = const getVersion
+
 doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()
 doQuestionToMeta _ = withCurrentBuffer questionToMeta