From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [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 ####. --- tools/fake_ide.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tools/fake_ide.ml') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 932097607..4dad16fd8 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -247,16 +247,16 @@ let eval_print l coq = let to_id, need_unfocus = get_id id in after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in - eval_call (query (phrase, to_id)) coq + eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> let phrase = "Stm Wait." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"JOIN") ] -> let phrase = "Stm JoinDocument." in - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" -- cgit v1.2.3