This strikes me as very similar to an iPython or Jupyter notebook, but for coq. Perhaps there might be something gained by using that existing infra with coq?