On Fri, Jul 8, 2016 at 5:35 AM, Enrico Tassi <enrico.ta...@inria.fr> wrote:
> On Fri, Jul 08, 2016 at 10:10:49AM +0200, Pierre Courtieu wrote:
>> I think it is available. But I a mnot sure we should reflect async
>> proof yet. Let us have PG work as before, then we make the async proof
>> queue working.
> As far as I know, Paul already reached that milestone!
Yes, the basic protocol is working (though it certainly needs
testing). In addition, I have a for-now-hackish way of using the
feedback messages to color spans in the case of errors, so some part
of the async feature is working.
> From his question, I imagine he is trying to support the "fixing a
> broken proof without retracting everything" feature provided by the XML
Yes, I was looking at the retraction induced by editing.
> Currently, the situation is alway one of the following two:
> 1) as usual, many locked spans followed by unprocessed text
> 2) a single proof, and only one, is under focus:
> all the spans before the proof are locked
> all the spans after the proof are locked
> eventually some unprocessed text after that
If I understand, then, if there are multiple proofs in a script
already processed, and I start editing an early file, retracting to
the point of editing will undo only the sentences within that proof.
All spans in subsequent proofs are still locked. That's situation (2).
Once I've finished editing that proof, and Add'ing all its sentences,
we're back in situation (1).
Consider this scenario. Again, I have multiple proofs in a file that
have been processed (situation (1)). Now I put the cursor somewhere in
an early proof and click the Goto button. Should that undo everything
past that point, as happens currently in PG, and leaves us in
situation (1), or should it be like editing at that same point, so
that we're again in situation (2)?
Maybe there should be two kinds of Goto, to distinguish these possibilities?
> To clarify, here I'm talking about the *locked* attribute of spans.
> The async mode needs other attributes (i.e. the red color) to be eventually
> attached later on to spans, and error tool tips eventually.
Emacs overlays, which are used to implement PG spans, have a
`help-echo' property for tooltips. I'll add the error text there.
ProofGeneral-devel mailing list