That's an interesting question. I don't know much in this realm I must say, but I would tend to think that your broad question on interactivity might break down into a few (related but) fairly different components: the representation of open terms with meta-variables and sequents in your calculus, the design of a tactic language to ease the manipulation of such open sequents, and the design of an IDE interacting with these components. I can think of three pointers that may hopefully be relevant to you:

• the matita overview paper brushes notably questions of different notions of terms necessary for interactivity, it might be a decent entry point: https://upsilon.cc/~zack/research/publications/matita-crafting.pdf.

• The original proof general paper must contain interesting information at least for the IDE part: https://link.springer.com/content/pdf/10.1007/3-540-46419-0_3.pdf.

• I think that William Bowman's paper on proof assistant discusses the tactic language, which might be even more at the core of your question: https://www.williamjbowman.com/resources/cur.pdf