Ide_intf: remove useless int answer to the "interp" and "rewind" calls

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

5 files changed, 35 insertions, 49 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index f04dfeede..c34c8f525 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -44,9 +44,9 @@ end
 
 val raw_interp : coqtop -> string -> unit Ide_intf.value
 
-val interp : coqtop -> bool -> string -> int Ide_intf.value
+val interp : coqtop -> bool -> string -> unit Ide_intf.value
 
-val rewind : coqtop -> int -> int Ide_intf.value
+val rewind : coqtop -> int -> unit Ide_intf.value
 
 val read_stdout : coqtop -> string Ide_intf.value
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e87f50016..2437a6112 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -82,7 +82,7 @@ object('self)
   method send_to_coq :
     bool -> bool -> string ->
       bool -> bool -> bool ->
-	(bool*int) option
+	bool option
   method set_message : string -> unit
   method show_goals : unit
   method show_goals_full : unit
@@ -833,7 +833,7 @@ object(self)
       prerr_endline "Send_to_coq starting now";
       match Coq.interp mycoqtop verbosely phrase with
         | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
-        | Ide_intf.Good r ->
+        | Ide_intf.Good () ->
           match Coq.read_stdout mycoqtop with
             | Ide_intf.Fail (_,str) ->
               self#set_message
@@ -841,7 +841,11 @@ object(self)
               None
             | Ide_intf.Good msg ->
               sync display_output msg;
-              Some (true,r)
+	      (* TODO: restore the access to Decl_mode.get_daemon_flag, and
+		 also detect if an admit has been used. Answering "false"
+		 in these cases would trigger a particular coloring
+		 (cf. Tags.Script.unjustified) *)
+              Some true
     with
       | e ->
         sync display_error (Coq.process_exn e); None
@@ -909,7 +913,7 @@ object(self)
         input_view#set_editable true;
         pop_info ();
       end in
-    let mark_processed reset_info is_complete (start,stop) =
+    let mark_processed is_complete (start,stop) =
       let b = input_buffer in
       b#move_mark ~where:stop (`NAME "start_of_input");
       b#apply_tag
@@ -929,14 +933,14 @@ object(self)
           None -> false
         | Some (loc,phrase) ->
           (match self#send_to_coq verbosely false phrase true true true with
-            | Some (is_complete,reset_info) ->
-              sync (mark_processed reset_info is_complete) loc; true
+            | Some is_complete ->
+              sync (mark_processed is_complete) loc; true
             | None -> sync remove_tag loc; false)
     end
 
   method insert_this_phrase_on_success
     show_output show_msg localize coqphrase insertphrase =
-    let mark_processed reset_info is_complete =
+    let mark_processed is_complete =
       let stop = self#get_start_of_input in
       if stop#starts_line then
         input_buffer#insert ~iter:stop insertphrase
@@ -977,8 +981,8 @@ object(self)
 	 | _ -> ())
 	 with _ -> ()*) in
     match self#send_to_coq false false coqphrase show_output show_msg localize with
-      | Some (is_complete,reset_info) ->
-        sync (mark_processed reset_info) is_complete; true
+      | Some is_complete ->
+        sync mark_processed is_complete; true
       | None ->
         sync
           (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
@@ -1057,7 +1061,7 @@ object(self)
               ("Error while backtracking :\n" ^ str ^ "\n" ^
 	       "CoqIDE and coqtop may be out of sync," ^
 	       "you may want to use Restart.")
-          | Ide_intf.Good _ ->
+          | Ide_intf.Good () ->
             sync (fun _ ->
               let start =
                 if Stack.is_empty cmd_stack then input_buffer#start_iter
@@ -1122,7 +1126,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          ignore ((Coq.rewind mycoqtop 1));
+          ignore (Coq.rewind mycoqtop 1);
           sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
@@ -1209,7 +1213,7 @@ object(self)
 		| Ide_intf.Fail (l,str) ->
 		  self#set_message
 		    ("Couln't add loadpath:\n"^str)
-		| Ide_intf.Good _ -> ()
+		| Ide_intf.Good () -> ()
   end
 
   method electric_handler =
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index a0bf5e429..1836fd299 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -26,29 +26,14 @@ 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) : int call =
-  Interp (b,s)
-
-let rewind i : int call =
-  Rewind i
-
-let read_stdout : string call =
-  Read_stdout
-
-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 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 read_stdout : string call = Read_stdout
+let current_goals : goals call = Cur_goals
+let current_status : string call = Cur_status
+let make_cases s : string list list call = Cases s
 
 (** * Coq answers to CoqIde *)
 
@@ -61,8 +46,8 @@ type 'a value =
 type handler = {
   is_in_loadpath : string -> bool;
   raw_interp : string -> unit;
-  interp : bool * string -> int;
-  rewind : int -> int;
+  interp : bool * string -> unit;
+  rewind : int -> unit;
   read_stdout : unit -> string;
   current_goals : unit -> goals;
   current_status : unit -> string;
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index b94846405..5039395a8 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -17,8 +17,8 @@ type goals =
 type 'a call
 
 val raw_interp : string -> unit call
-val interp : bool * string -> int call
-val rewind : int -> int call
+val interp : bool * string -> unit call
+val rewind : int -> unit call
 val is_in_loadpath : string -> bool call
 val make_cases : string -> string list list call
 (** The status, for instance "Ready in SomeSection, proving Foo" *)
@@ -38,8 +38,8 @@ type 'a value =
 type handler = {
   is_in_loadpath : string -> bool;
   raw_interp : string -> unit;
-  interp : bool * string -> int;
-  rewind : int -> int;
+  interp : bool * string -> unit;
+  rewind : int -> unit;
   read_stdout : unit -> string;
   current_goals : unit -> goals;
   current_status : unit -> string;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index b6a7906e2..b29618c17 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -247,8 +247,7 @@ let parsable_of_string s =
 let eval_expr loc_ast =
   let rewind_info = compute_reset_info loc_ast in
   Vernac.eval_expr loc_ast;
-  Stack.push rewind_info com_stk;
-  Stack.length com_stk
+  Stack.push rewind_info com_stk
 
 let raw_interp s =
   Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None))
@@ -277,10 +276,9 @@ let interp (verbosely,s) =
     if not (is_vernac_goal_printing_command vernac) then
       (* Verbose if in small step forward and not a tactic *)
       Flags.make_silent (not verbosely);
-    let stack_depth = eval_expr (loc,vernac) in
+    eval_expr (loc,vernac);
     Flags.make_silent true;
     prerr_endline ("...Done with interp of : "^s);
-    stack_depth
   with Vernac.End_of_input -> assert false
 
 let rewind count =
@@ -336,8 +334,7 @@ let rewind count =
             end
           end
   in
-  do_rewind count NoReset current_proofs None;
-  Stack.length com_stk
+  do_rewind count NoReset current_proofs None
 
 let is_in_loadpath dir =
   Library.is_in_load_paths (System.physical_path_of_string dir)