lean-mode icon indicating copy to clipboard operation
lean-mode copied to clipboard
verified publisher icon leanprover

Difficulty writing multi-line comments due to autocompletion

Open lenianiva opened this issue 2 years ago • 0 comments

When writing a multi-line comment like

/--
 Line 1
 Line 2
 ...
 -/

Suppose the user types in /---/ and places the cursor before the last -. Pressing enter there will result in

/---/
/-[CURSOR]-/

This makes it very cumbersome to write multiline comments. Is there a way to disable this behaviour?

lenianiva avatar Mar 15 '23 04:03 lenianiva