[vc] generalize range extraction

Fixes several issues regarding ranges extraction (option -x):

• some parts are still not collected ; must decompose proof terms structurally
• parts belonging to the same function/lemma shall be reported
• latest hypotheses (largest line number) shall also be reported (included in previous item)
• use multiple window (wrt context) to report sparse parts
• report line numbers
• colored keywords & comments