Reprocess whole buffer after each error

[proofbot]

Note: the issue was imported automatically using json2github.py

Original issue: psteckler/ProofGeneral#103 Opened by: @ybertot

I am using version 15972ca3ca80146eefc4cf16889934a111d7711a with coq-8.7

Here is an example:

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq tuple.
From mathcomp Require Import choice path finset finfun fintype bigop fingraph.
From mathcomp Require Import ssralg ssrnum matrix mxalgebra.
From mathcomp Require Import all_algebra.
(* From mathcomp Require Import finmap. *)
From mathcomp Require Import zmodp.

Require Import triangulation_algorithm.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory Num.Theory.

Lemma toto : forall l k, l <= k.+1 -> l <= k \/ l = k.+1.
Proof.
move => l k.

Execute all this to the end, nothing bad occurs, but if the next command fails for example, by trying

rewrite leq_eqV.

Then all lines become light blue, but not the whole buffer, and the next restarts from the very first line of the buffer.

[proofbot]

Comment author: @psteckler

I can reproduce the error, investigating.

[proofbot]

Comment author: @psteckler

@ybertot I've pushed a fix.

When processing that last line, the error should cause a retraction to the previous line, and the error on the last line should get highlighted in red.

Please try it!