aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:16 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:16 +0000
commit0692216822e1fd9001f15178c5cb9dd91c9fbc74 (patch)
treefb5bb8dcc5c92115078d039b78627fd1ce4bdb50 /ide
parent4c65f9a13758e5378026de77cfe5600e2dae8a73 (diff)
Ide_intf: slight reorganisation of the IDE api
- merge raw_interp with interp (with one more flag) - merge read_stdout with interp, which now return a string - shorter command names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/command_windows.ml10
-rw-r--r--ide/coq.ml19
-rw-r--r--ide/coq.mli13
-rw-r--r--ide/coqide.ml31
4 files changed, 30 insertions, 43 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 739435df4..0d0894213 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -102,15 +102,11 @@ object(self)
in
try
result#buffer#set_text
- (match Coq.raw_interp coqtop phrase with
+ (match Coq.interp coqtop ~raw:true phrase with
| Ide_intf.Fail (l,str) ->
("Error while interpreting "^phrase^":\n"^str)
- | Ide_intf.Good () ->
- match Coq.read_stdout coqtop with
- | Ide_intf.Fail (l,str) ->
- ("Error while fetching "^phrase^"results:\n"^str)
- | Ide_intf.Good results ->
- ("Result for command " ^ phrase ^ ":\n" ^ results))
+ | Ide_intf.Good results ->
+ ("Result for command " ^ phrase ^ ":\n" ^ results))
with e ->
let s = Printexc.to_string e in
assert (Glib.Utf8.validate s);
diff --git a/ide/coq.ml b/ide/coq.ml
index dbb0d8ac3..a5b2d38ab 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -199,13 +199,12 @@ let eval_call coqtop (c:'a Ide_intf.call) =
flush coqtop.cin;
(Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
-let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s))
-let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
-let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout
+let interp coqtop ?(raw=false) ?(verbose=true) s =
+ eval_call coqtop (Ide_intf.interp (raw,verbose,s))
let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
-let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
-let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s)
-let current_status coqtop = eval_call coqtop Ide_intf.current_status
+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
module PrintOpt =
struct
@@ -227,8 +226,8 @@ struct
List.fold_left
(fun acc cmd ->
let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
- match raw_interp coqtop str with
- | Ide_intf.Good () -> acc
+ match interp coqtop ~raw:true ~verbose:false str with
+ | Ide_intf.Good _ -> acc
| Ide_intf.Fail (l,errstr) -> Ide_intf.Fail (l,"Could not eval \""^str^"\": "^errstr)
)
(Ide_intf.Good ())
@@ -242,8 +241,8 @@ struct
state_hack (Ide_intf.Good ())
end
-let current_goals coqtop =
+let goals coqtop =
match PrintOpt.enforce_hack coqtop with
- | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals
+ | Ide_intf.Good () -> eval_call coqtop Ide_intf.goals
| Ide_intf.Fail str -> Ide_intf.Fail str
diff --git a/ide/coq.mli b/ide/coq.mli
index 04155ac40..685bfcac3 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -45,14 +45,13 @@ val interrupter : (int -> unit) ref
(** * Calls to Coqtop, cf [Ide_intf] for more details *)
-val interp : coqtop -> bool -> string -> unit Ide_intf.value
-val raw_interp : coqtop -> string -> unit Ide_intf.value
-val read_stdout : coqtop -> string Ide_intf.value
+val interp :
+ coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
val rewind : coqtop -> int -> unit Ide_intf.value
-val is_in_loadpath : coqtop -> string -> bool Ide_intf.value
-val make_cases : coqtop -> string -> string list list Ide_intf.value
-val current_status : coqtop -> string Ide_intf.value
-val current_goals : coqtop -> Ide_intf.goals Ide_intf.value
+val status : coqtop -> string Ide_intf.value
+val goals : coqtop -> Ide_intf.goals Ide_intf.value
+val inloadpath : coqtop -> string -> bool Ide_intf.value
+val mkcases : coqtop -> string -> string list list Ide_intf.value
(** A specialized version of [raw_interp] dedicated to
set/unset options. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f5321486..7a714b1d0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -829,7 +829,7 @@ object(self)
else
(fun _ _ -> ()) in
try
- match Coq.current_goals !mycoqtop with
+ match Coq.goals !mycoqtop with
| Ide_intf.Fail (l,str) ->
self#set_message ("Error in coqtop :\n"^str)
| Ide_intf.Good goals ->
@@ -842,7 +842,7 @@ object(self)
method show_goals = self#show_goals_full
- method private send_to_coq ct verbosely phrase show_output show_error localize =
+ method private send_to_coq ct verbose phrase show_output show_error localize =
let display_output msg =
self#insert_message (if show_output then msg else "") in
let display_error (loc,s) =
@@ -873,16 +873,11 @@ 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 verbosely phrase with
+ match Coq.interp ct ~verbose phrase with
| Ide_intf.Fail (l,str) -> sync display_error (l,str); None
- | Ide_intf.Good () ->
- match Coq.read_stdout ct with
- | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
- | Ide_intf.Good msg ->
- sync display_output msg;
- (** TODO: Restore someday the access to Decl_mode.get_damon_flag,
- and also detect the use of admit, and then return Unsafe *)
- Some Safe
+ | Ide_intf.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
@@ -1253,24 +1248,22 @@ object(self)
(input_view#event#connect#key_press ~callback:self#active_keypress_handler);
prerr_endline "CONNECTED active : ";
print_id (match act_id with Some x -> x | None -> assert false);
- match
- filename
- with
+ match filename with
| None -> ()
| Some f ->
let dir = Filename.dirname f in
let ct = !mycoqtop in
- match Coq.is_in_loadpath ct dir with
+ match Coq.inloadpath ct dir with
| Ide_intf.Fail (_,str) ->
self#set_message
("Could not determine lodpath, this might lead to problems:\n"^str)
| Ide_intf.Good true -> ()
| Ide_intf.Good false ->
let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
- match Coq.interp ct false cmd with
+ match Coq.interp ct cmd with
| Ide_intf.Fail (l,str) ->
self#set_message ("Couln't add loadpath:\n"^str)
- | Ide_intf.Good () -> ()
+ | Ide_intf.Good _ -> ()
end
method private electric_paren tag =
@@ -2180,7 +2173,7 @@ let main files =
ignore (f av);
pop_info ();
push_info
- (match Coq.current_status !(current.toplvl) with
+ (match Coq.status !(current.toplvl) with
| Ide_intf.Fail (l,str) ->
"Oops, problem while fetching coq status."
| Ide_intf.Good str -> str)
@@ -2195,7 +2188,7 @@ let main files =
let w = get_current_word () in
let cur_ct = !(session_notebook#current_term.toplvl) in
try
- match Coq.make_cases cur_ct w with
+ match Coq.mkcases cur_ct w with
| Ide_intf.Fail _ -> raise Not_found
| Ide_intf.Good cases ->
let print_branch c l =