How to partition Coq code to feed Coq ideslave (XML protocol)?

I thought the "Add" call of Coq ideslave (also known as Coq XML protocol) takes one chunk of code at a time, partitioned by periods (.). I still believe this to be true in most cases. For example,

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B

where "A \/ B" := (or A B) : type_scope.

Despite this code block has several lines, it should be fed in by one "Add" call, since only the last line has a period.

However, this isn't the case when bullets (+, -, *, {, and }) are present. For example,

- intros [H _]; exact H.

should be fed in by two "Add" calls, - and intros [H _]; exact H. In another case,

{ destruct Hl; [ right | destruct Fl | ]; assumption. }

should be fed in as three parts, {, destruct Hl; [ right | destruct Fl | ]; assumption., and }. I observed these behaviors in CoqIDE, which I think uses Coq ideslave internally.

My first question: are these the complete rules for partitioning a .v file into chunks for the use of "Add" calls? If no, what are the complete rules?

Second question: if I only use the "partitioned-by-period" rule, say if I try to feed { destruct Hl; [ right | destruct Fl | ]; assumption. } as one "Add" call instead of three, the XML won't raise an error immediately. However, after several proof steps, it could raise an error (This proof is focused, but cannot be unfocused this way) which never appear in Coq IDE, and I cannot undo the error by

<call val="Edit_at">
    <state_id val="..."/>
</call>

If I try to undo the error, the Coq XML gives the same error message. Is this error related to feeding the bullets as one chunk? If yes, why won't the Coq XML complain about this once I feed the chunk?

An additional question: I would like to try SerAPI in the near future. Does SerAPI share the same rules of feeding code chunks?

Thank you so much for helping!

Solution

Jim, in fact, splitting Coq commands is a non-trivial task, I'd say that the de-facto method is the one that CoqIDE uses, see CoqIDE's lexer, also this mail, Emacs' regexp, and CodeMirror's tokenizer.

For the Add call of the protocol, you should send a single sentence! The rest is ignored, and indeed, sentences do include braces. That is where your problem originated.

SerAPI does indeed include additional support to help tools with splitting. The most important differences are:

when you submit a single sentence, SerAPI will reply with the actual end of sentence location. Thus, you can parse a Coq document accurately by letting SerAPI do the splitting.
SerAPI can parse a complete Coq document in one go (and will reply back with the splitting locations).

There are some more technical details regarding the full-document support, but these should be better addressed at the project's page.