Improvements have been made in Coq 1.5 which make this unnecessary: using the PIDE system (originally from Isabelle) you can now throw the whole file at Coq, then send it diffs as the user makes edits. No need to rewind, go-to, etc.
I've used this in jEdit ( http://coqpide.bitbucket.org/ ) but there's also an Eclipse system built on it too ( https://coqoon.github.io/cav2015/ )
I might wait a little for my benchmarks to be 8.5 ready though!
On the other hand, One common problem in large proofs is having too many hypothesis in stock, one super nice extension would be to quantify the relevance of each and color/display them accordingly, leaving the option to move the 'tolerance' threshold for display. This relevance metric would have to be aware if lemmas available (of A -> B is proved by a lemma, and B is the goal, A is relevant).
My 2 cts.
For your other issue, I am thinking about ways to hide hypotheses in the editor, without having to clear them in the actual code. This way they are still here if you need them, but they don't eat some of your precious brain space while they are irrelevant (huh) to your current work.
Thanks for your 2 cts! Maybe I'll think about this threshold idea now!
Good job. :)
