CoqIDE ported to the revides protocol

- the zone to be edited is now between the marks
  start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
  a focused zone

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index be35ebe1a..96a19f317 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -370,7 +370,7 @@ let handle_final_answer handle xml =
     | None -> raise AnswerWithoutRequest
     | Some (c, _) -> c in
   let () = handle.waiting_for <- None in
-  with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer xml c) }
+  with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) }
 
 type input_state = {
   mutable fragment : string;
@@ -558,9 +558,9 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s =
-  eval_call ~logger (Serialize.interp (i,raw,verbose,s))
-let backto i = eval_call (Serialize.backto i)
+let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x)
+let edit_at i = eval_call (Serialize.edit_at i)
+let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
 let status ?logger force = eval_call ?logger (Serialize.status force)