what should the `#help note` message look like?

Stream: mathlib4

[Edward van de Meent]

in the discussion on batteries#948 , we were discussing how #help note "some label" should format library notes. We would like some input or opinions as to what would be preferred.
this is what a message from #help note "te" currently might look like:

library_note "temporary note"
/-
1: This is a testnote whose label also starts with "te", but gets sorted before "test"
-/

library_note "test"
/-
1: This is a testnote for testing the library note feature of batteries.
The `#help note` command should be able to find this note when imported.
-/

/-
2: This is a second testnote for testing the library note feature of batteries.
-/

/-
3: this is a note in a different file importing the above testnotes,
but still imported by the actual testfile.
-/

/-
4: This note was not imported, and therefore appears below the imported notes.
-/

/-
5: This note was also not imported, and therefore appears below the imported notes,
and the previously added note.
-/

note the heading with library_note "label" for each matching label, and the delineation with /- and -/ of individual notes.

[Eric Wieser]

Ideally the note would be markdown-rendered

[Edward van de Meent]

i'd like to note that the above code block is merely the text that the command generates as an info message, whether it gets rendered using markdown is afaik not up to the command...

[Eric Wieser]

I believe info messages can contain widgets

[Mario Carneiro]

no they cannot

[Mario Carneiro]

widgets appear as separate things from messages

[Mario Carneiro]

this is one of the reasons Try this produces two message-like things with slightly different formatting

[Eric Wieser]

Then why is Lean.MessageData.ofWidget a thing?

[Mario Carneiro]

...it wasn't a thing not long ago, maybe things have changed while I was not looking

[Mario Carneiro]

seems to have been merged in May

[Mario Carneiro]

while try this main implementation was May 2023

[Eric Wieser]

Yes, sorry, I should have mentioned that. I agree that "Try this" used what was available at the time.

[Edward van de Meent]

i think markdown may be in scope down the line, for now we'd like to know what people think the pure text version should look like...

[Edward van de Meent]

or at least, right now my goal is just to get any version of this merged into batteries, and if people think making it look nice is important enough, that can be added later.

[Edward van de Meent]

having done a bit of digging, it doesn't seem like there is a preexisting widget for displaying something as markdown in the infoview...

[Edward van de Meent]

and i don't think i'd be the best person for writing such a widget.