aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:09:54 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:09:54 +0000
commita4b5461afbd698b148e11eae003cb4e64bc92af3 (patch)
treebe4704b9ddf81dfcc173d164aebd9cba2638c18a /tools
parent56c4b269dcfb724b08bbcb37e814fe97ccf034f5 (diff)
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
Diffstat (limited to 'tools')
-rw-r--r--tools/fake_ide.ml13
1 files changed, 7 insertions, 6 deletions
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 ()));