diff options
| author | Maxime Dénès | 2017-06-20 10:47:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 10:47:40 +0200 |
| commit | 9c5378131c90c7fb819743d8e79c226492a0331f (patch) | |
| tree | 444f14b11613ebd90d7a9d154cd484f6624b6753 /tools | |
| parent | 6cae6006a95ca7587180a1293ab41d48877e79ea (diff) | |
| parent | d8874dd855d748aaaf504890487ab15ffd7a677d (diff) | |
Merge PR#774: [ide] Add route_id parameter to query call.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 932097607b..4dad16fd8c 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" |