Ide_intf: documentation of calls + debug printing of calls/answers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13941 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 59 insertions, 13 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 1836fd299a..7f3e593244 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -26,11 +26,11 @@ type 'a call =
   | Cur_status
   | Cases of string
 
-let is_in_loadpath s : bool call = In_loadpath s
-let raw_interp s : unit call = Raw_interp s
 let interp (b,s) : unit call = Interp (b,s)
-let rewind i : unit call = Rewind i
+let raw_interp s : unit call = Raw_interp s
 let read_stdout : string call = Read_stdout
+let rewind i : unit call = Rewind i
+let is_in_loadpath s : bool call = In_loadpath s
 let current_goals : goals call = Cur_goals
 let current_status : string call = Cur_status
 let make_cases s : string list list call = Cases s
@@ -44,11 +44,11 @@ type 'a value =
   | Fail of (location * string)
 
 type handler = {
-  is_in_loadpath : string -> bool;
-  raw_interp : string -> unit;
   interp : bool * string -> unit;
-  rewind : int -> unit;
+  raw_interp : string -> unit;
   read_stdout : unit -> string;
+  rewind : int -> unit;
+  is_in_loadpath : string -> bool;
   current_goals : unit -> goals;
   current_status : unit -> string;
   make_cases : string -> string list list;
@@ -69,3 +69,19 @@ let abstract_eval_call handler explain_exn c =
   with e ->
     let (l,str) = explain_exn e in
     Fail (l,str)
+
+(** * Debug printing *)
+
+let pr_call = function
+  | In_loadpath s -> "In_loadpath["^s^"]"
+  | Raw_interp s -> "Raw_interp["^s^"]"
+  | Interp (b,s) -> "Interp["^(if b then "true" else "false")^","^s^"]"
+  | Rewind i -> "Rewind["^(string_of_int i)^"]"
+  | Read_stdout -> "Read_stdout"
+  | Cur_goals -> "Cur_goals"
+  | Cur_status -> "Cur_status"
+  | Cases s -> "Cases["^s^"]"
+
+let pr_value = function
+  | Good _ -> "Good"
+  | Fail (_,str) -> "Fail["^str^"]"
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 5039395a8a..0a96e4d667 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** * Interface of calls to Coq by CoqIde *)
+(** * Interface of CoqIde calls to Coq *)
 
 type 'a menu = 'a * (string * string) list
 
@@ -16,16 +16,33 @@ type goals =
 
 type 'a call
 
-val raw_interp : string -> unit call
+(** Running a command. The boolean is a verbosity flag.
+    Output will be fetch later via [read_stdout]. *)
 val interp : bool * string -> unit call
+
+(** Running a command with no impact on the undo stack,
+    such as a query or a Set/Unset.
+    Output will be fetch later via [read_stdout]. *)
+val raw_interp : string -> unit call
+
+(** What messages have been displayed by coqtop recently ? *)
+val read_stdout : string call
+
+(** Backtracking by a certain number of phrases. *)
 val rewind : int -> unit call
+
+(** Is a file present somewhere in Coq's loadpath ? *)
 val is_in_loadpath : string -> bool call
+
+(** Create a "match" template for a given inductive type *)
 val make_cases : string -> string list list call
+
 (** The status, for instance "Ready in SomeSection, proving Foo" *)
 val current_status : string call
+
+(** Fetching the list of current goals *)
 val current_goals : goals call
-(** What has been displayed by coqtop recently ? *)
-val read_stdout : string call
+
 
 (** * Coq answers to CoqIde *)
 
@@ -36,11 +53,11 @@ type 'a value =
   | Fail of (location * string)
 
 type handler = {
-  is_in_loadpath : string -> bool;
-  raw_interp : string -> unit;
   interp : bool * string -> unit;
-  rewind : int -> unit;
+  raw_interp : string -> unit;
   read_stdout : unit -> string;
+  rewind : int -> unit;
+  is_in_loadpath : string -> bool;
   current_goals : unit -> goals;
   current_status : unit -> string;
   make_cases : string -> string list list;
@@ -49,3 +66,8 @@ type handler = {
 val abstract_eval_call :
   handler -> (exn -> location * string) ->
   'a call -> 'a value
+
+(** * Debug printing *)
+
+val pr_call : 'a call -> string
+val pr_value : 'a value -> string
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index b29618c177..4d7b8f5291 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -546,6 +546,11 @@ let eval_call c =
   in
   Ide_intf.abstract_eval_call handler handle_exn c
 
+let pr_debug s =
+  if !Flags.debug then begin
+    Printf.eprintf "[pid %d] %s\n" (Unix.getpid ()) s; flush stderr
+  end
+
 (** Exceptions during eval_call should be converted into Ide_intf.Fail
     messages by explain_exn above. Otherwise, we die badly, after having
     tried to send a last message to the ide: trying to recover from errors
@@ -559,11 +564,14 @@ let loop () =
   try
     while true do
       let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
+      pr_debug ("<-- " ^ Ide_intf.pr_call q);
       let r = eval_call q in
+      pr_debug ("--> " ^ Ide_intf.pr_value r);
       Marshal.to_channel !orig_stdout r []; flush !orig_stdout
     done
   with e ->
     let msg = Printexc.to_string e in
     let r = Ide_intf.Fail (None, "Fatal exception in coqtop:\n" ^ msg) in
+    pr_debug ("==> " ^ Ide_intf.pr_value r);
     (try Marshal.to_channel !orig_stdout r []; flush !orig_stdout with _ -> ());
     exit 1