diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 11:41:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-18 03:44:16 +0200 |
| commit | d8874dd855d748aaaf504890487ab15ffd7a677d (patch) | |
| tree | bfc4b7173c489388fd650a2bd10e4e5de0719287 /stm/vernac_classifier.ml | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (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 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e45..d25861d5a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -30,9 +30,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b,(id,route)) -> - "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ - " route " ^ string_of_int route + | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b @@ -92,8 +90,7 @@ let rec classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater + | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -213,7 +210,6 @@ let rec classify_vernac e = make_polymorphic res else res -let classify_as_query = - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater +let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater |