nomeata / loogle

Mathlib search tool
https://loogle.lean-lang.org/
Apache License 2.0
63 stars 8 forks source link

copy-pasting from VSCode behavior #22

Open fpvandoorn opened 6 days ago

fpvandoorn commented 6 days ago

If I copy-paste text from VSCode into the Loogle search bar, and the search bar is already non-empty, two unexpected things happen:

This behavior is easily visible if you copy text in VSCode and then paste it multiple times in the Loogle search bar.

I am using Windows & Firefox.

nomeata commented 6 days ago

Hmm, can’t reproduce on Firefox and Linux. Does it depend on what you are copying, e.g. if it involves unicode or backslashes or so?

fpvandoorn commented 6 days ago

Nope, it can be any word or a single letter, highlighted or not. I expect that it has to do with the fact that some markup is copied with it.

FWIW: I also cannot reproduce this on Windows + Chrome...

E.g. if I copy AddAction from VSCode, and paste it a couple times in Chrome I get

AddActionAddActionAddActionAddActionAddActionAddActionAddActionAddAction

in Firefox I get

AddAction AddActio AddActio AddActio AddActio AddActio AddActio
AddAction
n n n n n n

Only when copying it here I notice that there's even newlines in there...