Merge pull request #156 from iwashis/master

autoOne functionality update for Agda v2.7.0 and up
isovector · Oct 24, 2024 · 41b7d5e · 41b7d5e
2 parents 06d6020 + 80059af
commit 41b7d5e
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 13 deletions.
diff --git a/src/Cornelis/Types/Agda.hs b/src/Cornelis/Types/Agda.hs
@@ -136,8 +136,8 @@ data Interaction' range
   | Cmd_solveOne Rewrite InteractionId range String
 
     -- | Solve (all goals / the goal at point) by using Auto.
-  | Cmd_autoOne            InteractionId range String
-  | Cmd_autoAll
+  | Cmd_autoOne  Rewrite InteractionId range String
+  | Cmd_autoAll  Rewrite
 
     -- | Parse the given expression (as if it were defined at the
     -- top-level of the current module) and infer its type.

diff --git a/src/Lib.hs b/src/Lib.hs
@@ -205,7 +205,7 @@ cornelis = do
         , $(command "CornelisLoad"             'doLoad)             [CmdSync Async]
         , $(command "CornelisGoals"            'doAllGoals)         [CmdSync Async]
         , $(command "CornelisSolve"            'solveOne)           [CmdSync Async, rw_complete]
-        , $(command "CornelisAuto"             'autoOne)            [CmdSync Async]
+        , $(command "CornelisAuto"             'autoOne)            [CmdSync Async, rw_complete]
         , $(command "CornelisTypeInfer"        'doTypeInfer)        [CmdSync Async]
         , $(command "CornelisTypeContext"      'typeContext)        [CmdSync Async, rw_complete]
         , $(command "CornelisTypeContextInfer" 'typeContextInfer)   [CmdSync Async, rw_complete]

diff --git a/src/Plugin.hs b/src/Plugin.hs
@@ -150,16 +150,18 @@ solveOne _ ms = withNormalizationMode ms $ \mode ->
         (mkAbsPathRnage fp $ ip_interval' ip)
         ""
 
-autoOne :: CommandArguments -> Neovim CornelisEnv ()
-autoOne _ = withAgda $ void $ withGoalAtCursor $ \b ip -> do
-  agda <- getAgda b
-  t <- getGoalContents b ip
-  fp <- buffer_get_name b
-  flip runIOTCM agda $
-    Cmd_autoOne
-      (ip_id ip)
-      (mkAbsPathRnage fp $ ip_interval' ip)
-      (T.unpack t)
+autoOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()
+autoOne _ ms = withNormalizationMode ms $ \mode ->
+  withAgda $ void $ withGoalAtCursor $ \b ip -> do
+    agda <- getAgda b
+    t <- getGoalContents b ip
+    fp <- buffer_get_name b
+    flip runIOTCM agda $
+      Cmd_autoOne
+        mode
+        (ip_id ip)
+        (mkAbsPathRnage fp $ ip_interval' ip)
+        (T.unpack t)
 
 withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()
 withNormalizationMode Nothing f = normalizationMode >>= f