loogle generates invalid request

Stream: mathlib4

[Kenny Lau]

In loogle#CategoryStruct.comp (CategoryTheory.Limits.pullback.map _ _ _ _ _ _ _ _) (CategoryTheory.Limits.pullback.fst _ _), loogle thinks that the first thing should be CategoryTheory.CategoryStruct.comp, but in the generated link, the spaces are changed to %20 instead of +, which generates an "invalid request"

[Kenny Lau]

I suppose I should ping @Joachim Breitner

[Robin Arnez]

The problem is the %0A (a newline), not the %20. Also, when you "fix" it, you get:

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

[Robin Arnez]

Oh actually there is one too few _ in your original request as well

[Joachim Breitner]

Ah, the problem is that loogle rejects queries with \n (mostly as a defense against users trying to mess with it), but the suggestions come out of the pretty printer, and that seems to add line breaks for long queries.

Fixed by pretty-printing with a large width.