From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- ide/command_windows.ml | 10 +++++----- ide/coq.ml | 12 ++++++------ ide/coq.mli | 2 +- ide/coqide.ml | 11 +++++------ 4 files changed, 17 insertions(+), 18 deletions(-) (limited to 'ide') 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 _ -> () -- cgit v1.2.3