search

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

"Fill goal" works incorrectly in presence of ==<, >== and `qed #263

Open marat-rkh opened 3 years ago

marat-rkh commented 3 years ago

Invoke "Fill goal" on the following code:

Screen Shot 2021-04-19 at 11 18 09 AM

Expected result:

Screen Shot 2021-04-19 at 11 18 54 AM

Actual result:

Screen Shot 2021-04-19 at 11 18 34 AM

Note that `qed lost its `. Also the last {?} is after the qed, not before it. These are bugs.

ice1000 commented 3 years ago

It's the pretty printer

valis commented 3 years ago

I thought it just syntactically inserts the expression. Why does it invoke pretty printer?

ice1000 commented 3 years ago

Oh, sorry, I remembered it wrongly.

ice1000 commented 3 years ago

https://github.com/JetBrains/intellij-arend/blob/1c110f1081154aa297aeb8f3a0e8af0c48803965/src/main/kotlin/org/arend/quickfix/GoalFillingQuickFix.kt#L13