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

3 files changed, 141 insertions, 127 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 7f3e59324..5374b06df 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -16,24 +16,23 @@ type goals =
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
+type raw = bool
+type verbose = bool
+
 type 'a call =
-  | In_loadpath of string
-  | Raw_interp of string
-  | Interp of bool * string
+  | Interp of raw * verbose * string
   | Rewind of int
-  | Read_stdout
-  | Cur_goals
-  | Cur_status
-  | Cases of string
-
-let interp (b,s) : unit call = Interp (b,s)
-let raw_interp s : unit call = Raw_interp s
-let read_stdout : string call = Read_stdout
+  | Goals
+  | Status
+  | InLoadPath of string
+  | MkCases of string
+
+let interp (r,b,s) : string call = Interp (r,b,s)
 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
+let goals : goals call = Goals
+let status : string call = Status
+let inloadpath s : bool call = InLoadPath s
+let mkcases s : string list list call = MkCases s
 
 (** * Coq answers to CoqIde *)
 
@@ -44,27 +43,23 @@ type 'a value =
   | Fail of (location * string)
 
 type handler = {
-  interp : bool * string -> unit;
-  raw_interp : string -> unit;
-  read_stdout : unit -> string;
+  interp : raw * verbose * string -> string;
   rewind : int -> unit;
-  is_in_loadpath : string -> bool;
-  current_goals : unit -> goals;
-  current_status : unit -> string;
-  make_cases : string -> string list list;
+  goals : unit -> goals;
+  status : unit -> string;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
 }
 
 let abstract_eval_call handler explain_exn c =
   try
     let res = match c with
-      | In_loadpath s -> Obj.magic (handler.is_in_loadpath s)
-      | Raw_interp s -> Obj.magic (handler.raw_interp s)
-      | Interp (b,s) -> Obj.magic (handler.interp (b,s))
+      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s))
       | Rewind i -> Obj.magic (handler.rewind i)
-      | Read_stdout -> Obj.magic (handler.read_stdout ())
-      | Cur_goals -> Obj.magic (handler.current_goals ())
-      | Cur_status -> Obj.magic (handler.current_status ())
-      | Cases s -> Obj.magic (handler.make_cases s)
+      | Goals -> Obj.magic (handler.goals ())
+      | Status -> Obj.magic (handler.status ())
+      | InLoadPath s -> Obj.magic (handler.inloadpath s)
+      | MkCases s -> Obj.magic (handler.mkcases s)
     in Good res
   with e ->
     let (l,str) = explain_exn e in
@@ -73,15 +68,30 @@ let abstract_eval_call handler explain_exn c =
 (** * 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^"]"
+  | Interp (r,b,s) ->
+    let raw = if r then "RAW" else "" in
+    let verb = if b then "" else "SILENT" in
+    "INTERP"^raw^verb^" ["^s^"]"
+  | Rewind i -> "REWIND "^(string_of_int i)
+  | Goals -> "GOALS"
+  | Status -> "STATUS"
+  | InLoadPath s -> "INLOADPATH "^s
+  | MkCases s -> "MKCASES "^s
+
+let pr_value_gen pr = function
+  | Good v -> "GOOD " ^ pr v
+  | Fail (_,str) -> "FAIL ["^str^"]"
+
+let pr_value v = pr_value_gen (fun _ -> "") v
+
+let pr_string s = "["^s^"]"
+let pr_bool b = if b then "true" else "false"
+
+let pr_full_value call value =
+  match call with
+    | Interp _ -> pr_value_gen pr_string (Obj.magic value)
+    | Rewind i -> pr_value value
+    | Goals -> pr_value value (* TODO *)
+    | Status -> pr_value_gen pr_string (Obj.magic value)
+    | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value)
+    | MkCases s -> pr_value value (* TODO *)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index bd92460f2..211b34e13 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -16,34 +16,36 @@ type goals =
 
 type 'a 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
+type raw = bool
+type verbose = bool
+
+(** Running a command (given as a string).
+    - The 1st flag indicates whether to use "raw" mode
+      (less sanity checks, no impact on the undo stack).
+      Suitable e.g. for queries, or for the Set/Unset
+      of display options that coqide performs all the time.
+    - The 2nd flag controls the verbosity.
+    - The returned string contains the messages produced
+      by this command, but not the updated goals (they are
+      to be fetch by a separated [current_goals]). *)
+val interp : raw * verbose * string -> 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
+(** Fetching the list of current goals *)
+val goals : goals call
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+val status : string call
+
+(** Is a directory part of Coq's loadpath ? *)
+val inloadpath : string -> bool call
 
 (** Create a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
     followed by enough pattern variables. *)
-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
+val mkcases : string -> string list list call
 
 
 (** * Coq answers to CoqIde *)
@@ -54,15 +56,15 @@ type 'a value =
   | Good of 'a
   | Fail of (location * string)
 
+(** * The structure that coqtop should implement *)
+
 type handler = {
-  interp : bool * string -> unit;
-  raw_interp : string -> unit;
-  read_stdout : unit -> string;
+  interp : raw * verbose * string -> string;
   rewind : int -> unit;
-  is_in_loadpath : string -> bool;
-  current_goals : unit -> goals;
-  current_status : unit -> string;
-  make_cases : string -> string list list;
+  goals : unit -> goals;
+  status : unit -> string;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
 }
 
 val abstract_eval_call :
@@ -73,3 +75,4 @@ val abstract_eval_call :
 
 val pr_call : 'a call -> string
 val pr_value : 'a value -> string
+val pr_full_value : 'a call -> 'a value -> string
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index c7667f030..616cd5b09 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -25,6 +25,27 @@ let init_signal_handler () =
 
 let prerr_endline _ = ()
 
+let orig_stdout = ref stdout
+
+let init_stdout,read_stdout =
+  let out_buff = Buffer.create 100 in
+  let out_ft = Format.formatter_of_buffer out_buff in
+  let deep_out_ft = Format.formatter_of_buffer out_buff in
+  let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
+  (fun () ->
+     flush_all ();
+     orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout);
+     Unix.dup2 Unix.stderr Unix.stdout;
+     Pp_control.std_ft := out_ft;
+     Pp_control.err_ft := out_ft;
+     Pp_control.deep_ft := deep_out_ft;
+     set_binary_mode_out !orig_stdout true;
+     set_binary_mode_in stdin true;
+  ),
+  (fun () -> Format.pp_print_flush out_ft ();
+             let r = Buffer.contents out_buff in
+             Buffer.clear out_buff; r)
+
 let coqide_known_option table = List.mem table [
   ["Printing";"Implicit"];
   ["Printing";"Coercions"];
@@ -242,41 +263,42 @@ let compute_reset_info loc_ast =
     loc_ast = loc_ast;
   }
 
-let parsable_of_string s =
-  Pcoq.Gram.parsable (Stream.of_string s)
+(** Check whether a command is forbidden by CoqIDE *)
+
+let coqide_cmd_checks (loc,ast) =
+  let user_error s =
+    raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s)))
+  in
+  if is_vernac_debug_command ast then
+    user_error "Debug mode not available within CoqIDE";
+  if is_vernac_navigation_command ast then
+    user_error "Use CoqIDE navigation instead";
+  if is_vernac_known_option_command ast then
+    user_error "Use CoqIDE display menu instead";
+  if is_vernac_query_command ast then
+    msgerrnl (str "Warning: query commands should not be inserted in scripts")
+
+let raw_eval_expr = Vernac.eval_expr
 
 let eval_expr loc_ast =
   let rewind_info = compute_reset_info loc_ast in
-  Vernac.eval_expr loc_ast;
+  raw_eval_expr loc_ast;
   Stack.push rewind_info com_stk
 
-let raw_interp s =
-  Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None))
-
-let user_error_loc l s =
-    raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s)))
-
-let interp (verbosely,s) =
+let interp (raw,verbosely,s) =
   prerr_endline "Starting interp...";
   prerr_endline s;
-  let pa = parsable_of_string s in
-  try
-    let (loc,vernac) = Vernac.parse_sentence (pa,None) in
-    if is_vernac_debug_command vernac then
-      user_error_loc loc (str "Debug mode not available within CoqIDE");
-    if is_vernac_navigation_command vernac then
-      user_error_loc loc (str "Use CoqIDE navigation instead");
-    if is_vernac_known_option_command vernac then
-      user_error_loc loc (str "Use CoqIDE display menu instead");
-    if is_vernac_query_command vernac then
-      msgerrnl (str "Warning: query commands should not be inserted in scripts");
-    if not (is_vernac_goal_printing_command vernac) then
-      (* Verbose if in small step forward and not a tactic *)
-      Flags.make_silent (not verbosely);
-    eval_expr (loc,vernac);
-    Flags.make_silent true;
-    prerr_endline ("...Done with interp of : "^s);
-  with Vernac.End_of_input -> assert false
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let loc_ast = Vernac.parse_sentence (pa,None) in
+  if not raw then coqide_cmd_checks loc_ast;
+  (* Verbose if command is not a tactic and IDE said to be verbose
+     (i.e. we're in small step forward mode) *)
+  Flags.make_silent
+    (is_vernac_goal_printing_command (snd loc_ast) || not verbosely);
+  if raw then raw_eval_expr loc_ast else eval_expr loc_ast;
+  Flags.make_silent true;
+  prerr_endline ("...Done with interp of : "^s);
+  read_stdout ()
 
 let rewind count =
   let undo_ops = Hashtbl.create 31 in
@@ -333,7 +355,7 @@ let rewind count =
   in
   do_rewind count NoReset current_proofs None
 
-let is_in_loadpath dir =
+let inloadpath dir =
   Library.is_in_load_paths (System.physical_path_of_string dir)
 
 let string_of_ppcmds c =
@@ -388,7 +410,7 @@ let concl_next_tac sigma concl =
     "right"
   ])
 
-let current_goals () =
+let goals () =
   try
     let pfts =
       Proof_global.give_me_the_proof ()
@@ -430,7 +452,7 @@ let current_goals () =
   with Proof_global.NoCurrentProof ->
     Ide_intf.Message "" (* quick hack to have a clean message screen *)
 
-let current_status () =
+let status () =
   (** We remove the initial part of the current [dir_path]
       (usually Top in an interactive session, cf "coqtop -top"),
       and display the other parts (opened sections and modules) *)
@@ -447,27 +469,6 @@ let current_status () =
   in
   "Ready"^path^proof
 
-let orig_stdout = ref stdout
-
-let init_stdout,read_stdout =
-  let out_buff = Buffer.create 100 in
-  let out_ft = Format.formatter_of_buffer out_buff in
-  let deep_out_ft = Format.formatter_of_buffer out_buff in
-  let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
-  (fun () ->
-     flush_all ();
-     orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout);
-     Unix.dup2 Unix.stderr Unix.stdout;
-     Pp_control.std_ft := out_ft;
-     Pp_control.err_ft := out_ft;
-     Pp_control.deep_ft := deep_out_ft;
-     set_binary_mode_out !orig_stdout true;
-     set_binary_mode_in stdin true;
-  ),
-  (fun () -> Format.pp_print_flush out_ft ();
-             let r = Buffer.contents out_buff in
-             Buffer.clear out_buff; r)
-
 let explain_exn e =
   let toploc,exc =
     match e with
@@ -480,6 +481,8 @@ let explain_exn e =
   toploc,(Errors.print exc)
 
 let eval_call c =
+  (* If the messages of last command are still there, we remove them *)
+  ignore (read_stdout ());
   let rec handle_exn e =
     catch_break := false;
     match e with
@@ -498,14 +501,12 @@ let eval_call c =
     r
   in
   let handler = {
-    Ide_intf.is_in_loadpath = interruptible is_in_loadpath;
-    Ide_intf.raw_interp = interruptible raw_interp;
     Ide_intf.interp = interruptible interp;
     Ide_intf.rewind = interruptible rewind;
-    Ide_intf.read_stdout = interruptible read_stdout;
-    Ide_intf.current_goals = interruptible current_goals;
-    Ide_intf.current_status = interruptible current_status;
-    Ide_intf.make_cases = interruptible Vernacentries.make_cases }
+    Ide_intf.goals = interruptible goals;
+    Ide_intf.status = interruptible status;
+    Ide_intf.inloadpath = interruptible inloadpath;
+    Ide_intf.mkcases = interruptible Vernacentries.make_cases }
   in
   Ide_intf.abstract_eval_call handler handle_exn c
 
@@ -529,7 +530,7 @@ let loop () =
       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);
+      pr_debug ("--> " ^ Ide_intf.pr_full_value q r);
       Marshal.to_channel !orig_stdout r []; flush !orig_stdout
     done
   with e ->