From a4b5461afbd698b148e11eae003cb4e64bc92af3 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 30 Sep 2013 16:09:54 +0000 Subject: fake_ide ported to the new protocol (FIXME tests fail) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/fake_ide.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 19a82d6ea..13151598b 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -31,7 +31,7 @@ let base_eval_call call coqtop = loop () else if Serialize.is_feedback xml then loop () - else (Serialize.to_answer xml call) + else (Serialize.to_answer call xml) in let res = loop () in prerr_endline (Serialize.pr_full_value call res); @@ -53,18 +53,19 @@ let rec erase_ids n = | [] -> exit 1 let eid = ref 0 let edit () = incr eid; !eid +let curid () = match !ids with x :: _ -> x | _ -> Stateid.initial let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (0,true,false,s))); - "INTERPRAW", (fun s -> eval_call (Serialize.interp (0,true,true,s))); + [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.query (s,Stateid.dummy))); + "INTERPRAW", (fun s -> eval_call (Serialize.query (s,Stateid.dummy))); "INTERPSILENT", (fun s c -> - store_id (base_eval_call (Serialize.interp (edit(),false,false,s)) c)); + store_id (base_eval_call (Serialize.add ((s,edit()),(curid(),false))) c)); "INTERP", (fun s c -> - store_id (base_eval_call (Serialize.interp (edit(),false,true,s)) c)); + store_id (base_eval_call (Serialize.add ((s,edit()),(curid(),true))) c)); "REWIND", (fun s -> let i = int_of_string s in let id = erase_ids i in - eval_call (Serialize.backto id)); + eval_call (Serialize.edit_at id)); "GOALS", (fun _ -> eval_call (Serialize.goals ())); "HINTS", (fun _ -> eval_call (Serialize.hints ())); "GETOPTIONS", (fun _ -> eval_call (Serialize.get_options ())); -- cgit v1.2.3