add debugging option

Author: 4e554c4c

README.md

@@ -167,7 +167,19 @@ text objects to behave.
 
 `ih`/`ah` will operate on `{!` and `!}`.
 
+### Debugging
 
+When debugging the cornelis plugin or creating an issue, set the `cornelis_debug` variable.
+
+```viml
+let g:cornelis_debug = v:true
+```
+
+```lua
+vim.g.cornelis_debug = true
+```
+
+Cornelis will then output agda interaction information to `/tmp/agda.log`.
 
 ## Installation
 

src/Cornelis/Agda.hs

@@ -5,10 +5,10 @@ module Cornelis.Agda where
 
 import           Control.Concurrent.Chan.Unagi (newChan, readChan, writeChan)
 import           Control.Lens
-import           Control.Monad (forever, replicateM_, when)
+import           Control.Monad (forever, replicateM_)
 import           Control.Monad.IO.Class
 import           Control.Monad.State
-import           Cornelis.Debug (reportExceptions)
+import           Cornelis.Debug (reportExceptions, debugString)
 import           Cornelis.InfoWin (buildInfoBuffer)
 import           Cornelis.Types
 import           Cornelis.Types.Agda
@@ -28,9 +28,8 @@ import           System.Process
 
 ------------------------------------------------------------------------------
 -- | When true, dump out received JSON as it arrives.
-debugJson :: Bool
-debugJson = False
-
+debugJson :: Neovim CornelisEnv Bool
+debugJson = asks $ cc_debug . ce_config
 
 ------------------------------------------------------------------------------
 -- | Create an 'Agda' environment for the given buffer. This spawns an
@@ -70,7 +69,7 @@ spawnAgda buffer = do
           Right res -> do
             case res of
               HighlightingInfo _ _ -> pure ()
-              _ -> when debugJson $ vim_report_error $ T.pack $ show resp
+              _ -> whenM debugJson $ debugString $ LT.unpack resp
             liftIO $ writeChan chan $ AgdaResp buffer res
 
       void $ neovimAsync $ liftIO $ forever $ do

src/Cornelis/Config.hs

@@ -4,7 +4,7 @@ module Cornelis.Config where
 
 import           Cornelis.Types
 import           Cornelis.Types.Agda (Rewrite(..))
-import           Cornelis.Utils (objectToInt, objectToText)
+import           Cornelis.Utils (objectToInt, objectToText, objectToBool)
 import           Data.Maybe (fromMaybe)
 import qualified Data.Text as T
 import           Neovim
@@ -40,5 +40,6 @@ getConfig
     <*> (fromMaybe Horizontal . (>>= (readSplitLocation . T.unpack <=< objectToText)) <$>
         getVarWithAlternatives ["cornelis_split_location", "cornelis_split_direction"])
     <*> (fromMaybe HeadNormal . (>>= (readRewrite . T.unpack <=< objectToText)) <$>
-        (getVar "cornelis_rewrite_mode"))
+        getVar "cornelis_rewrite_mode")
+    <*> (fromMaybe False . (objectToBool =<<) <$> getVar "cornelis_debug")
 

src/Cornelis/Debug.hs

@@ -15,11 +15,15 @@ traceMX :: Show a => String -> a -> Neovim env ()
 traceMX herald a =
   vim_report_error $ "!!!" <> herald <> ": " <> show a
 
-debug :: (Show a, MonadIO m) => a -> m ()
-debug x = liftIO $ go 100
+debugString :: MonadIO m => String -> m ()
+debugString s = liftIO $ go 100
   where
     go 0 = pure ()
     go n =
       catch
-       (appendFile  "/tmp/agda.log" (show x <> "\n"))
+       (appendFile  "/tmp/agda.log" (s <> "\n"))
        (\e -> if isAlreadyInUseError e then go (n-1 :: Int) else throw e)
+
+
+debug :: (Show a, MonadIO m) => a -> m ()
+debug = debugString . show

src/Cornelis/Types.hs

@@ -116,6 +116,7 @@ data CornelisConfig = CornelisConfig
   , cc_max_width :: Int64
   , cc_split_location :: SplitLocation
   , cc_rewrite_mode :: Rewrite
+  , cc_debug :: Bool
   }
   deriving (Show, Generic)
 

src/Cornelis/Utils.hs

@@ -31,6 +31,13 @@ objectToText :: Object -> Maybe Text
 objectToText (ObjectString w) = Just $ decodeUtf8 w
 objectToText _ = Nothing
 
+objectToBool :: Object -> Maybe Bool
+objectToBool (ObjectBool b) = Just b
+objectToBool o = objectToInt @Int o >>= \case
+    0 -> Just False
+    1 -> Just True
+    _ -> Nothing
+
 neovimAsync :: (MonadUnliftIO m) => m a -> m (Async a)
 neovimAsync m =
   withRunInIO $ \lower ->