Brackets in comments cause problems with "Try this"

[shingtaklam1324]

import tactic

example (X : Type) (p : X → Prop) : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin
  library_search -- avoid smileys if you want to use "try this" :-)
end

example (X : Type) (p : X → Prop) : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin
  library_search -- and frownies are even worse :-(
end

Clicking on the "Try this:" code doesn't work, because the system gets confused by the brackets (in the first case the comment is deleted apart from the bracket; in the second case end gets deleted too). In practice I guess one isn't going to write anything after library_search usually -- the only reason I ran into this was because I was documenting something for a beginner.

---

Originally opened by @kbuzzard as leanprover-community/mathlib#5051

[bryangingechen]

The relevant part of the code starts here, if anyone wants to take a crack at it: https://github.com/leanprover/vscode-lean/blob/master/src/tacticsuggestions.ts#L79