Load only when Agda is idle, and save on load

phijor · Jan 13, 2023 · b2ec8ae · b2ec8ae
1 parent 3ff9321
commit b2ec8ae
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 17 deletions.
diff --git a/src/Cornelis/Agda.hs b/src/Cornelis/Agda.hs
@@ -14,6 +14,7 @@ import           Cornelis.Types
 import           Cornelis.Types.Agda
 import           Cornelis.Utils
 import           Data.Aeson
+import           Data.IORef
 import qualified Data.Map as M
 import qualified Data.Text as T
 import qualified Data.Text.Lazy as LT
@@ -43,18 +44,28 @@ spawnAgda buffer = do
       (proc "agda" ["--interaction-json"])
         { std_in = CreatePipe , std_out = CreatePipe }
   (c_in, c_out) <- liftIO newChan
+  ready <- liftIO $ newIORef True
   case (m_in, m_out) of
     (Just hin, Just hout) -> do
       liftIO $ do
         hSetBuffering hin NoBuffering
         hSetBuffering hout NoBuffering
 
-      void $ neovimAsync $ forever $ reportExceptions $ do
+      let whenReady act = liftIO $ do
+            -- Agda outputs "JSON> " when it is ready
+            -- We skip it, and set the ready flag
+            c <- hLookAhead hout
+            case c of
+              'J' -> replicateM_ 6 (hGetChar hout) >> act
+              _ -> pure ()
+
+      -- On the first load, we make ourselves ready before Agda tells us anything
+      void $ neovimAsync $ (whenReady (pure ()) >>) . forever $ reportExceptions $ do
+        whenReady $ atomicWriteIORef ready True
         resp <- liftIO $ hGetLine hout
         chan <- asks ce_stream
-        let resp' = dropPrefix "JSON> " resp
-        case eitherDecode @Response $ encodeUtf8 resp' of
-          _ | LT.null resp' -> pure ()
+        case eitherDecode @Response $ encodeUtf8 resp of
+          _ | LT.null resp -> pure ()
           Left err -> vim_report_error $ T.pack err
           Right res -> do
             case res of
@@ -64,9 +75,10 @@ spawnAgda buffer = do
 
       void $ neovimAsync $ liftIO $ forever $ do
         msg <- readChan c_out
+        atomicWriteIORef ready False
         hPutStrLn hin msg
 
-      pure $ Agda buffer c_in hdl
+      pure $ Agda buffer ready c_in hdl
     (_, _) -> error "can't start agda"
 
 

diff --git a/src/Cornelis/Types.hs b/src/Cornelis/Types.hs
@@ -44,6 +44,7 @@ deriving stock instance Ord Buffer
 
 data Agda = Agda
   { a_buffer :: Buffer
+  , a_ready  :: IORef Bool
   , a_req    :: InChan String
   , a_hdl    :: ProcessHandle
   }

diff --git a/src/Lib.hs b/src/Lib.hs
@@ -59,7 +59,7 @@ respond b (InteractionPoints ips) = do
 -- Replace a function clause
 respond b (MakeCase mkcase) = do
   doMakeCase b mkcase
-  reload
+  load
 -- Replace the interaction point with a result
 respond b (GiveAction result ip) = do
   let i = ip_id ip
@@ -68,7 +68,7 @@ respond b (GiveAction result ip) = do
     Just ip' -> do
       int <- getIpInterval b ip'
       replaceInterval b int $ replaceQuestion result
-  reload
+  load
 -- Replace the interaction point with a result
 respond b (SolveAll solutions) = do
   for_ solutions $ \(Solution i ex) ->
@@ -77,7 +77,7 @@ respond b (SolveAll solutions) = do
       Just ip -> do
         int <- getIpInterval b ip
         replaceInterval b int $ replaceQuestion ex
-  reload
+  load
 respond b ClearHighlighting = do
   -- delete what we know about goto positions and stored extmarks
   modifyBufferStuff b $ \bs -> bs

diff --git a/src/Plugin.hs b/src/Plugin.hs
@@ -22,6 +22,7 @@ import           Cornelis.Utils
 import           Cornelis.Vim
 import           Data.Bool (bool)
 import           Data.Foldable (for_, fold, toList)
+import           Data.IORef (readIORef)
 import           Data.List
 import qualified Data.Map as M
 import           Data.Ord
@@ -64,21 +65,19 @@ gotoDefinition = withAgda $ do
       vim_command $ "keepjumps normal! " <> T.pack (show buffer_idx) <> "go"
 
 
-reload :: Neovim CornelisEnv ()
-reload = do
-  vim_command "noautocmd w"
-  load
-
-
 doLoad :: CommandArguments -> Neovim CornelisEnv ()
 doLoad = const load
 
 
 load :: Neovim CornelisEnv ()
 load = withAgda $ withCurrentBuffer $ \b -> do
   agda <- getAgda b
-  name <- buffer_get_name $ a_buffer agda
-  flip runIOTCM agda $ Cmd_load name []
+  ready <- liftIO $ readIORef $ a_ready agda
+  if ready then do
+    vim_command "noautocmd w"
+    name <- buffer_get_name $ a_buffer agda
+    flip runIOTCM agda $ Cmd_load name []
+  else vim_report_error "Agda is busy, not ready to load"
 
 questionToMeta :: Buffer -> Neovim CornelisEnv ()
 questionToMeta b = withBufferStuff b $ \bs -> do
@@ -100,7 +99,7 @@ questionToMeta b = withBufferStuff b $ \bs -> do
 
   -- Force a save if we replaced any goals
   case getAny res of
-    True -> reload
+    True -> load
     False -> pure ()