В документе Coq XML Protocol (для Добавить операцию), строка имеет вид <int>${editId}</int>
. Что такое editID здесь?
Я спросил об этом, потому что мне не удалось взаимодействовать с coqtop в режиме ideslave. Используя coq-8.6.1/theories/FSets/FSetCompat.v
в качестве примера, я ввел
<call val="Init"><option val="none"/></call>
,
<call val="Add"><pair><pair><string>Require Import FSetInterface FSetFacts MSetInterface MSetFacts.</string><int>1</int></pair><pair><state_id val="1"/><bool val="true"/></pair></pair></call>
,
<call val="Add"><pair><pair><string>Set Implicit Arguments.</string><int>1</int></pair><pair><state_id val="2"/><bool val="true"/></pair></pair></call>
, а потом
<call val="Add"><pair><pair><string>Unset Strict Implicit.</string><int>1</int></pair><pair><state_id val="3"/><bool val="true"/></pair></pair></call>
Все они генерировали правильные результаты. Однако в это время, когда я набрал
<call val="Add"><pair><pair><string>Module Backport_WSets
(E:DecidableType.DecidableType)
(M:MSetInterface.WSets with Definition E.t := E.t
with Definition E.eq := E.eq)
<: FSetInterface.WSfun E.</string><int>1</int></pair><pair><state_id val="4"/><bool val="true"/></pair></pair></call>
Я получил следующую ошибку:
[pid 48519] XML syntax error: Attribute value expected
[pid 48519] XML syntax error: Xml node expected
[pid 48519] XML syntax error: Xml node expected
[pid 48519] Unexpected XML message
[pid 48519] Expected XML node: call
[pid 48519] XML tree received: <int>1</int>
[pid 48519] XML syntax error: Xml node expected
[pid 48519] Unexpected XML message
[pid 48519] Expected XML node: call
[pid 48519] XML tree received: <pair>
<state_id val="4"/>
<bool val="true"/>
</pair>
[pid 48519] XML syntax error: Xml node expected
[pid 48519] XML syntax error: Xml node expected
Я подозреваю, что эта ошибка из-за многострочной строки, и, возможно, если я изменю editId, я должен получить правильный ответ. Я прав? Если нет, что делает editID и как мне справиться с этой ошибкой? Спасибо за помощь!
: FSetInterface.WSfun E.
?) - person greybeard   schedule 06.12.2017a less-than sign
о чудо! Разве это не должно быть<
? - person greybeard   schedule 06.12.2017<
на<
! Ошибка была не из-за разрыва строки, а из-за этого! - person Jian Wang   schedule 06.12.2017