diff options
author | 2017-12-27 10:20:14 +0100 | |
---|---|---|
committer | 2017-12-27 10:20:14 +0100 | |
commit | 2a25e1a56460556f8b8dcef2a70cd0d2b9422383 (patch) | |
tree | 0bd3a6f5ce21870abcdeb4373a54e21a3d469f75 | |
parent | 5cd3b9c6356ef3f35eddd3fa6d57375c92b09469 (diff) | |
parent | 6b09f69e4da3c1fd491dbc5b475195a95636f636 (diff) |
Merge PR #6507: [ide] [doc] Document tweak to Query call.
-rw-r--r-- | dev/doc/changes.md | 7 | ||||
-rw-r--r-- | dev/doc/xml-protocol.md | 6 |
2 files changed, 13 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 01aa6b599..f6fbb6942 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -68,6 +68,13 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### XML IDE Protocol + +- Before 8.8, `Query` only executed the first command present in the + `query` string; starting with 8.8, the caller may include several + statements. This is useful for instance for temporarily setting an + option and then executing a command. + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 18f6288f6..b35571e9c 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`. <string>${message}</string> </value> ``` + +Before 8.8, `Query` only executed the first command present in the +`query` string; starting with 8.8, the caller may include several +statements. This is useful for instance for temporarily setting an +option and then executing a command. + ------------------------------- |