From d941f739dd51f5702bccd8a61ed08027fb0fb264 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 21 Mar 2017 17:54:02 +0100 Subject: [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. --- stm/stm.ml | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) (limited to 'stm/stm.ml') 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 = -- cgit v1.2.3