banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

`C-c` `C-s` and `C-c` `C-a` inserts `\n` instead of newlines #158

Open fredrik-bakke opened 1 year ago

fredrik-bakke commented 1 year ago

What the title says. For instance, in the following case

image

Using C-c C-s will give

image

For this issue to be resolved, #159 should probably be resolved first, as otherwise the hole brackets must be manually removed.

banacorn commented 8 months ago

Please reopen this and provide an file for reproducing the problem if it still persists

fredrik-bakke commented 8 months ago

This problem seems to still persist. I will try to make an example when I'm at my computer and have the time.

ncfavier commented 6 months ago

The issue also occurs with C-c C-r. Here's a minimal reproducing example:

module Bug where

postulate
  A : Set

record Foo : Set where
  field
    very-long-field-name-1 : A
    very-long-field-name-2 : A
    very-long-field-name-3 : A

foo : Foo
foo = {! C-c C-r !}
-- foo = record\n{ very-long-field-name-1 = {!   !}\n; very-long-field-name-2 = {!   !}\n; very-long-field-name-3 = {!   !}\n}