diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:09:54 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-30 16:09:54 +0000 |
| commit | a4b5461afbd698b148e11eae003cb4e64bc92af3 (patch) | |
| tree | be4704b9ddf81dfcc173d164aebd9cba2638c18a /tools | |
| parent | 56c4b269dcfb724b08bbcb37e814fe97ccf034f5 (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.ml | 13 |
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 ())); |