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

[marat-rkh]

Invoke "Fill goal" on the following code:

Expected result:

Actual result:

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

[ice1000]

It's the pretty printer

[valis]

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

[ice1000]

Oh, sorry, I remembered it wrongly.

[ice1000]

intellij-arend/src/main/kotlin/org/arend/quickfix/GoalFillingQuickFix.kt

Line 13 in 1c110f1

replaceExprSmart(editor.document, element, null, element.textRange, expr, null, expr.text)