Change agsy to mimer

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.

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