ProofGeneral and qrhl-tool detect end of command differently.

[dominique-unruh]

Example: 90c0be2e9696bc1da8cebecad5752d5644119ab6 in dominique-unruh/compressed-oracle-formalization, file lemma_cr1_cr2_2.qrhl.

Problem: In case of a mix of different parens, emacs may consider an expression balanced that isn't according to qrhl-tool. Then it processes till the ., sends this to qrhl-tool. qrhl-tool sees the . inside an unfinished expression and waits for a continuation. Consequence: communication is terminally out of sync.

To solve, we should do two things:

• Give an understandable error in this case. (I think PG never sends commands as multiline strings, so if a partial command is sent in -emacs mode, then qrhl-tool is justified in raising an error.)
• Fix the PG recognition of end-of-command to match up parentheses exactly like qrhl-tool.

[dominique-unruh]

Rejecting partial commands when --emacs is given: c4cbb6a