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

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 =