Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

4 files changed, 17 insertions, 18 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 470bd5b4..d496e9fd 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -84,10 +84,6 @@ object(self)
 		  ~packing:hbox#pack
 		  ()
     in
-    let on_activate c () =
-      if List.mem combo#entry#text Coq_commands.state_preserving then c ()
-      else prerr_endline "Not a state preserving command"
-    in
     let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
     entry#misc#set_can_default true;
     let r_bin =
@@ -103,6 +99,10 @@ object(self)
     result#misc#modify_base [`NORMAL, `COLOR clr];
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
+    let on_activate c () =
+      if List.mem combo#entry#text Coq_commands.state_preserving then c ()
+      else result#buffer#set_text "Error: Not a state preserving command"
+    in
     let callback () =
       let com = combo#entry#text in
       let phrase =
@@ -111,7 +111,7 @@ object(self)
       in
       try
         result#buffer#set_text
-          (match Coq.interp !coqtop ~raw:true phrase with
+          (match Coq.interp !coqtop ~raw:true 0 phrase with
              | Interface.Fail (l,str) ->
                  ("Error while interpreting "^phrase^":\n"^str)
              | Interface.Good results ->
diff --git a/ide/coq.ml b/ide/coq.ml
index 07f0ece8..82cdc726 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -270,13 +270,13 @@ let eval_call coqtop (c:'a Ide_intf.call) =
   let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
   (Ide_intf.to_answer xml c : 'a Interface.value)
 
-let interp coqtop ?(raw=false) ?(verbose=true) s =
-  eval_call coqtop (Ide_intf.interp (raw,verbose,s))
+let interp coqtop ?(raw=false) ?(verbose=true) i s =
+  eval_call coqtop (Ide_intf.interp (i,raw,verbose,s))
 let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
 let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s)
 let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s)
-let status coqtop = eval_call coqtop Ide_intf.status
-let hints coqtop = eval_call coqtop Ide_intf.hints
+let status coqtop = eval_call coqtop (Ide_intf.status ())
+let hints coqtop = eval_call coqtop (Ide_intf.hints ())
 
 module PrintOpt =
 struct
@@ -308,8 +308,8 @@ end
 
 let goals coqtop =
   let () = PrintOpt.enforce_hack coqtop in
-  eval_call coqtop Ide_intf.goals
+  eval_call coqtop (Ide_intf.goals ())
 
 let evars coqtop =
   let () = PrintOpt.enforce_hack coqtop in
-  eval_call coqtop Ide_intf.evars
+  eval_call coqtop (Ide_intf.evars ())
diff --git a/ide/coq.mli b/ide/coq.mli
index f25268ef..0f40c61e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -47,7 +47,7 @@ val interrupter : (int -> unit) ref
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
 val interp :
-  coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
+  coqtop -> ?raw:bool -> ?verbose:bool -> int -> string -> string Interface.value
 val rewind : coqtop -> int -> int Interface.value
 val status : coqtop -> Interface.status Interface.value
 val goals : coqtop -> Interface.goals option Interface.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 94be8318..76094abe 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -868,11 +868,9 @@ object(self)
       prerr_endline "Send_to_coq starting now";
       (* It's important here to work with [ct] and not [!mycoqtop], otherwise
          we could miss a restart of coqtop and continue sending it orders. *)
-      match Coq.interp ct ~verbose phrase with
+      match Coq.interp ct ~verbose 0 phrase with
         | Interface.Fail (l,str) -> sync display_error (l,str); None
         | Interface.Good msg -> sync display_output msg; Some Safe
-          (* TODO: Restore someday the access to Decl_mode.get_damon_flag,
-	     and also detect the use of admit, and then return Unsafe *)
     with
       | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *)
         raise RestartCoqtop
@@ -890,9 +888,10 @@ object(self)
       end
     in
     try
-      match Coq.interp !mycoqtop ~raw:true ~verbose:false phrase with
+      match Coq.interp !mycoqtop ~raw:true ~verbose:false 0 phrase with
       | Interface.Fail (_, err) -> sync display_error err
-      | Interface.Good msg -> sync self#insert_message msg
+      | Interface.Good msg ->
+	sync self#insert_message msg
     with
     | End_of_file -> raise RestartCoqtop
     | e -> sync display_error (Printexc.to_string e)
@@ -1256,7 +1255,7 @@ object(self)
 	  | Interface.Good true -> ()
 	  | Interface.Good false ->
 	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-	    match Coq.interp ct cmd with
+	    match Coq.interp ct 0 cmd with
 	      | Interface.Fail (l,str) ->
 		self#set_message ("Couln't add loadpath:\n"^str)
 	      | Interface.Good _ -> ()