aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 17:54:02 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-16 05:34:25 +0100
commitd941f739dd51f5702bccd8a61ed08027fb0fb264 (patch)
tree198a4e7b31f0479431c067bf673c313ba88949ee /stm
parent50bd89748af03bb28ad7024f2ceef500489a91b0 (diff)
[stm] [ide protocol] Allow to include several commands on query.
This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml29
1 files changed, 19 insertions, 10 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 1d46e0833..3cb6bd9b6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2994,16 +2994,25 @@ let query ~doc ~at ~route s =
stm_purify (fun s ->
if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
else Reach.known_state ~cache:`Yes at;
- let loc, ast = parse_sentence ~doc at s in
- let indentation, strlen = compute_indentation ?loc at in
- CWarnings.set_current_loc loc;
- let clas = Vernac_classifier.classify_vernac ast in
- let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
- match clas with
- | VtMeta , _ -> (* TODO: can this still happen ? *)
- ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
- | _ ->
- ignore(process_transaction aast (VtQuery (false, route), VtNow)))
+ try
+ while true do
+ let loc, ast = parse_sentence ~doc at s in
+ let indentation, strlen = compute_indentation ?loc at in
+ CWarnings.set_current_loc loc;
+ let clas = Vernac_classifier.classify_vernac ast in
+ let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
+ match clas with
+ | VtMeta , _ -> (* TODO: can this still happen ? *)
+ ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
+ | _ ->
+ ignore(process_transaction aast (VtQuery (false,route), VtNow))
+ done;
+ with
+ | End_of_input -> ()
+ | exn ->
+ let iexn = CErrors.push exn in
+ Exninfo.iraise iexn
+ )
s
let edit_at ~doc id =