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, 2 insertions, 2 deletions

diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index a95b9f892..3422b1682 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -115,11 +115,11 @@ object(self)
       in
       let log level message = result#buffer#insert (message^"\n") in
       let process =
-	Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function
+	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
             result#buffer#insert str;
 	    Coq.return ()
-          | Interface.Good (_,res) ->
+          | Interface.Good res ->
             result#buffer#insert res; 
 	    Coq.return ())
       in