что такое editId в документе XML-протокола Coq?

В документе 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 и как мне справиться с этой ошибкой? Спасибо за помощь!


person Jian Wang    schedule 05.12.2017    source источник
comment
(Добро пожаловать в SO) (Что это за странный персонаж перед : FSetInterface.WSfun E.?)   -  person greybeard    schedule 06.12.2017
comment
@greybeard Спасибо! Это знак меньше.   -  person Jian Wang    schedule 06.12.2017
comment
a less-than sign о чудо! Разве это не должно быть &lt;?   -  person greybeard    schedule 06.12.2017
comment
@greybeard Да, ты прав! Ошибка была решена после того, как я изменил < на &lt;! Ошибка была не из-за разрыва строки, а из-за этого!   -  person Jian Wang    schedule 06.12.2017


Ответы (2)


EditId был удален в Coq 8.7; его первоначальная цель и история немного сложны из-за сложности протокола и исторических проблем.

А именно, операция Add является синхронной в том смысле, что пользовательский интерфейс должен ожидать ответа с новым назначенным идентификатором (Stateid.t) для добавленного диапазона.

Однако, если произошла ошибка синтаксического анализатора, асинхронной системе обратной связи требовался временной идентификатор, для этой цели служил edit_id.

Мы удалили edit_id, так как Add в любом случае является синхронным, поэтому для вызывающей стороны Add имеет смысл использовать синхронный обработчик ошибок вместо обратной связи на основе edit_id.

Обратите внимание, что я настоятельно не рекомендую использовать текущую синхронную версию Add. Это заставляет клиента внедрять сложную систему блокировки, и вскоре она будет заменена асинхронно-дружественной версией [где пользовательский интерфейс заранее выбирает span_id]. Такая версия уже доступна в ML API и предоставляется SerAPI (*) и, вероятно, самим протоколом XML, начиная с версии 8.8.

(*) Применяются обычные заявления об отказе от ответственности: я являюсь автором SerAPI, также обратите внимание, что я был лицом, стоящим за удалением edit_id из Coq 8.7.

person ejgallego    schedule 06.12.2017
comment
Спасибо за ваш ответ! Блокировка действительно неудобная. Я обошел это с помощью pty. Я должен попробовать ваш SerAPI в ближайшем будущем! Не могли бы вы сказать мне, почему возникла ошибка, когда я вводил многострочную строку с помощью «Добавить» (как показано в моем вопросе)? - person Jian Wang; 06.12.2017
comment
Вероятно, вам нужно закодировать разрыв строки с помощью и html-объекта? Поучительно посмотреть, что делает CoqIDE -debug. - person ejgallego; 06.12.2017
comment
Спасибо! @greybeard только что сказал мне изменить знак < на &lt;, после чего ошибка исчезла. Так что ошибка была не в разрывах строк. Спасибо за ваш ответ для edit_id! - person Jian Wang; 06.12.2017
comment
Да, вам нужно закодировать довольно много вещей, см. здесь текущие цитаты, используемые в самой CoqIDE: github.com/coq/coq/blob/v8.7/ide/xml_printer.ml#L19 - person ejgallego; 07.12.2017

Кажется, не помешает отправить editid вместо Add, даже в 8.7, даже если он не используется на стороне Coq.

Мой основанный на XML форк Proof General включает editid вместо Add с 8.7, и в результате не возникает никаких ошибок.

person Paul Steckler    schedule 06.12.2017
comment
Я думаю, что фактический вызов не был изменен, чтобы не беспокоить людей, но параметр игнорируется. - person ejgallego; 07.12.2017