The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

On 05/07/2013 09:39, Carst Tankink wrote:
> Based on Pierre's examples, I am not sure how you obtain feedback on
> 'state' in the -ideslave mode (I see a 'rewind' command that undoes a
> command, but do you have to synchronize this in your own IDE somehow?
> Especially since Coq's rewind can step back farther than instructed).

IDE have to do some work, rewind documentation is :

(** Backtracking by a certain number of (non-state-preserving) commands.
    This is used by Coqide.
    It may actually undo more commands than asked : for instance instead
    of jumping back in the middle of a finished proof, we jump back before
    this proof. The number of extra backtracked command is returned at
    the end. *)

Otherwise,
YES specification has to be made
YES a concrete syntax tree is much better than a string
YES it has to be adapted to asynchronous communication
YES ...
experimental attempts to do that are spread over the github forest. Time
has to be found to complete these tasks ...


Pierre B.