*bubble* showing tactic state in custom notation

[lecopivo]

I have a custom notation x:term "rewrite_by" c:convSeq which takes a term x and rewrites it by conv tactic c. I would like to have a bubble showing the tactic state right after rewrite_by similarly how there is a bubble right after by when you enter tactic mode.

For example here

#check (0 + 5 + 0) rewrite_by simp∘

there is a bubble(indicated by ∘) after simp but no bubble after rewrite_by.

I would like to have

#check (0 + 5 + 0) rewrite_by∘ simp∘

[david-christiansen]

This would be a useful thing to have!

How flexible would this API need to be for you? Is it overwhelming to have some kind of custom handler that lets you place them precisely where you want them for a given syntax kind? Or perhaps a set of kind-keyword pairs would be enough?

[lecopivo]

So far I have these notations where I have a custom by and it would be nice to have a bubble after it

notation term "rewrite_by" convSeq : term
notation "derive_random_approx" term "by" convSeq : term
notation "approx" ident bracketedBinder* ":=" term "by" tacticSeq : command

[david-christiansen]

Sounds like the latter would work for all these examples!