aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/xml-protocol.md
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 11:41:40 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-18 03:44:16 +0200
commitd8874dd855d748aaaf504890487ab15ffd7a677d (patch)
treebfc4b7173c489388fd650a2bd10e4e5de0719287 /dev/doc/xml-protocol.md
parent1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff)
[ide] Add route_id parameter to query call.
This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
Diffstat (limited to 'dev/doc/xml-protocol.md')
-rw-r--r--dev/doc/xml-protocol.md9
1 files changed, 7 insertions, 2 deletions
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 2ff82c688..127b4a6d2 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -308,15 +308,20 @@ CoqIDE typically sets `force` to `false`.
-------------------------------
+### <a name="command-query">**Query(route_id: integer, query: string, stateId: integer)**</a>
+
+`routeId` can be used to distinguish the result of a particular query,
+`stateId` should be set to the state the query should be run.
-### <a name="command-query">**Query(query: string, stateId: integer)**</a>
-In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state.
```html
<call val="Query">
<pair>
+ <route_id val="${routeId}"/>
+ <pair>
<string>${query}</string>
<state_id val="${stateId}"/>
</pair>
+ </pair>
</call>
```
#### *Returns*