Separated the toplevel interface into a purely declarative module with associated types (interface.mli), and an applicative part processing the calls (previous ide_intf).

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

11 files changed, 128 insertions, 173 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 0d0894213e..9792d8782f 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -103,9 +103,9 @@ object(self)
       try
         result#buffer#set_text
           (match Coq.interp coqtop ~raw:true phrase with
-             | Ide_intf.Fail (l,str) ->
+             | Interface.Fail (l,str) ->
                  ("Error while interpreting "^phrase^":\n"^str)
-             | Ide_intf.Good results ->
+             | Interface.Good results ->
                  ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let s = Printexc.to_string e in
diff --git a/ide/coq.ml b/ide/coq.ml
index 8c2e7105ce..77f3c44ae2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -206,7 +206,7 @@ let eval_call coqtop (c:'a Ide_intf.call) =
   Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
   flush coqtop.cin;
   let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
-  (Ide_intf.to_answer xml : 'a Ide_intf.value)
+  (Ide_intf.to_answer xml : 'a Interface.value)
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
   eval_call coqtop (Ide_intf.interp (raw,verbose,s))
@@ -237,22 +237,22 @@ struct
       (fun acc cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
          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)
+           | Interface.Good _ -> acc
+           | Interface.Fail (l,errstr) ->  Interface.Fail (l,"Could not eval \""^str^"\": "^errstr)
       )
-      (Ide_intf.Good ())
+      (Interface.Good ())
       opt
 
   let enforce_hack coqtop = Hashtbl.fold
     (fun opt v acc ->
       match set coqtop opt v with
-        | Ide_intf.Good () -> Ide_intf.Good ()
-        | Ide_intf.Fail str -> Ide_intf.Fail str)
-    state_hack (Ide_intf.Good ())
+        | Interface.Good () -> Interface.Good ()
+        | Interface.Fail str -> Interface.Fail str)
+    state_hack (Interface.Good ())
 end
 
 let goals coqtop =
   match PrintOpt.enforce_hack coqtop with
-    | Ide_intf.Good () -> eval_call coqtop Ide_intf.goals
-    | Ide_intf.Fail str -> Ide_intf.Fail str
+    | Interface.Good () -> eval_call coqtop Ide_intf.goals
+    | Interface.Fail str -> Interface.Fail str
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 3a92646500..eb26c60352 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -46,13 +46,13 @@ val interrupter : (int -> unit) ref
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
 val interp :
-  coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
-val rewind : coqtop -> int -> int Ide_intf.value
-val status : coqtop -> Ide_intf.status Ide_intf.value
-val goals : coqtop -> Ide_intf.goals Ide_intf.value
-val hints : coqtop -> (Ide_intf.hint list * Ide_intf.hint) option Ide_intf.value
-val inloadpath : coqtop -> string -> bool Ide_intf.value
-val mkcases : coqtop -> string -> string list list Ide_intf.value
+  coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
+val rewind : coqtop -> int -> int Interface.value
+val status : coqtop -> Interface.status Interface.value
+val goals : coqtop -> Interface.goals Interface.value
+val hints : coqtop -> (Interface.hint list * Interface.hint) option Interface.value
+val inloadpath : coqtop -> string -> bool Interface.value
+val mkcases : coqtop -> string -> string list list Interface.value
 
 (** A specialized version of [raw_interp] dedicated to
     set/unset options. *)
@@ -68,5 +68,5 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> t -> bool -> unit Ide_intf.value
+  val set : coqtop -> t -> bool -> unit Interface.value
 end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3e87ad3683..498660081e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -343,9 +343,9 @@ let setopts ct opts v =
   List.fold_left
     (fun acc o ->
       match Coq.PrintOpt.set ct o v with
-        | Ide_intf.Good () -> acc
-        | Ide_intf.Fail lstr -> Ide_intf.Fail lstr
-    ) (Ide_intf.Good ()) opts
+        | Interface.Good () -> acc
+        | Interface.Fail lstr -> Interface.Fail lstr
+    ) (Interface.Good ()) opts
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -830,12 +830,12 @@ object(self)
           (fun _ _ -> ()) in
       try
         match Coq.goals !mycoqtop with
-          | Ide_intf.Fail (l,str) ->
+          | Interface.Fail (l,str) ->
             self#set_message ("Error in coqtop :\n"^str)
-          | Ide_intf.Good goals ->
+          | Interface.Good goals ->
             let hints = match Coq.hints !mycoqtop with
-            | Ide_intf.Fail (_, _) -> None
-            | Ide_intf.Good hints -> hints
+            | Interface.Fail (_, _) -> None
+            | Interface.Good hints -> hints
             in
             Ideproof.display
               (Ideproof.mode_tactic menu_callback)
@@ -878,8 +878,8 @@ object(self)
       (* 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 ~verbose phrase with
-        | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
-        | Ide_intf.Good msg -> sync display_output msg; Some Safe
+        | Interface.Fail (l,str) -> sync display_error (l,str); None
+        | Interface.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
@@ -1117,7 +1117,7 @@ object(self)
 	  else n_pop (pred n)
     in
     match Coq.rewind !mycoqtop n with
-      | Ide_intf.Good n ->
+      | Interface.Good n ->
 	n_pop n;
         sync (fun _ ->
           let start =
@@ -1130,7 +1130,7 @@ object(self)
           self#show_goals;
           self#clear_message;
           finish start) ()
-      | Ide_intf.Fail (l,str) ->
+      | Interface.Fail (l,str) ->
         sync self#set_message
           ("Error while backtracking :\n" ^ str ^ "\n" ^
 	   "CoqIDE and coqtop may be out of sync, you may want to use Restart.")
@@ -1265,16 +1265,16 @@ object(self)
 	let dir = Filename.dirname f in
 	let ct = !mycoqtop in
 	match Coq.inloadpath ct dir with
-	  | Ide_intf.Fail (_,str) ->
+	  | Interface.Fail (_,str) ->
 	    self#set_message
 	      ("Could not determine lodpath, this might lead to problems:\n"^str)
-	  | Ide_intf.Good true -> ()
-	  | Ide_intf.Good false ->
+	  | Interface.Good true -> ()
+	  | Interface.Good false ->
 	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
 	    match Coq.interp ct cmd with
-	      | Ide_intf.Fail (l,str) ->
+	      | Interface.Fail (l,str) ->
 		self#set_message ("Couln't add loadpath:\n"^str)
-	      | Ide_intf.Good _ -> ()
+	      | Interface.Good _ -> ()
   end
 
   method private electric_paren tag =
@@ -2184,14 +2184,14 @@ let main files =
         ignore (f av);
         pop_info ();
         let msg = match Coq.status !(current.toplvl) with
-        | Ide_intf.Fail (l, str) ->
+        | Interface.Fail (l, str) ->
           "Oops, problem while fetching coq status."
-        | Ide_intf.Good status ->
-          let path = match status.Ide_intf.status_path with
+        | Interface.Good status ->
+          let path = match status.Interface.status_path with
           | None -> ""
           | Some p -> " in " ^ p
           in
-          let name = match status.Ide_intf.status_proofname with
+          let name = match status.Interface.status_proofname with
           | None -> ""
           | Some n -> ", proving " ^ n
           in
@@ -2210,8 +2210,8 @@ let main files =
     let cur_ct = !(session_notebook#current_term.toplvl) in
     try
       match Coq.mkcases cur_ct w with
-        | Ide_intf.Fail _ -> raise Not_found
-        | Ide_intf.Good cases ->
+        | Interface.Fail _ -> raise Not_found
+        | Interface.Good cases ->
           let print_branch c l =
 	    Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
 	      (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 61b9f73621..ddfc721e90 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -36,7 +36,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
 
 let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
   | [] -> assert false
-  | { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = cur_goal; } :: rem_goals ->
+  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
         proof#buffer#remove_tag
           ~start:proof#buffer#start_iter
@@ -86,7 +86,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         proof#buffer#insert ~tags (cur_goal ^ "\n")
       in
       (* Insert remaining goals (no hypotheses) *)
-      let fold_goal i _ { Ide_intf.goal_ccl = g } =
+      let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
         proof#buffer#insert (g ^ "\n")
       in
@@ -98,7 +98,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
 
 let mode_cesar (proof:GText.view) = function
   | [] -> assert false
-  | { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = cur_goal; } :: _ ->
+  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
       proof#buffer#insert "    *** Declarative Mode ***\n";
       List.iter
         (fun hyp -> proof#buffer#insert (hyp^"\n"))
@@ -110,22 +110,22 @@ let mode_cesar (proof:GText.view) = function
 let display mode (view:GText.view) goals hints =
   view#buffer#set_text "";
   match goals with
-    | Ide_intf.No_current_proof -> ()
-    | Ide_intf.Proof_completed ->
+    | Interface.No_current_proof -> ()
+    | Interface.Proof_completed ->
       view#buffer#insert "Proof Completed."
-    | Ide_intf.Unfocused_goals l ->
+    | Interface.Unfocused_goals l ->
       view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
       let iter goal =
-        let msg = Printf.sprintf "%s\n" goal.Ide_intf.goal_ccl in
+        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
       List.iter iter l
-    | Ide_intf.Uninstantiated_evars el ->
+    | Interface.Uninstantiated_evars el ->
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar in
         view#buffer#insert msg
       in
       List.iter iter el
-    | Ide_intf.Goals g ->
+    | Interface.Goals g ->
       mode view g hints
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 6ae5f7ea70..e06ebb78e8 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -23,7 +23,7 @@ let eval_call (call:'a Ide_intf.call) =
   let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
   let res = Ide_intf.to_answer xml_answer in
   prerr_endline (Ide_intf.pr_full_value call res);
-  match res with Ide_intf.Fail _ -> exit 1 | _ -> ()
+  match res with Interface.Fail _ -> exit 1 | _ -> ()
 
 let commands =
   [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s)));
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 7a3afa7fbf..29594b140c 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -9,35 +9,12 @@
 (** * Interface of calls to Coq by CoqIde *)
 
 open Xml_parser
+open Interface
 
 type xml = Xml_parser.xml
 
-type 'a menu = 'a * (string * string) list
-
-type status = {
-  status_path : string option;
-  status_proofname : string option;
-}
-
-type goal = {
-  goal_hyp : string list;
-  goal_ccl : string;
-}
-
-type goals =
-  | No_current_proof
-  | Proof_completed
-  | Unfocused_goals of goal list
-  | Uninstantiated_evars of string list
-  | Goals of goal list
-
-type hint = (string * string) list
-
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
-type raw = bool
-type verbose = bool
-
 type 'a call =
   | Interp of raw * verbose * string
   | Rewind of int
@@ -57,23 +34,6 @@ let mkcases s : string list list call = MkCases s
 
 (** * Coq answers to CoqIde *)
 
-type location = (int * int) option (* start and end of the error *)
-
-type 'a value =
-  | Good of 'a
-  | Fail of (location * string)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  handle_exn : exn -> location * string;
-}
-
 let abstract_eval_call handler c =
   try
     let res = match c with
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index cdd86f7946..ada6ffe224 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -6,34 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** * Interface of CoqIde calls to Coq *)
+(** * Applicative part of the interface of CoqIde calls to Coq *)
 
-type xml = Xml_parser.xml
-
-type goal = {
-  goal_hyp : string list;
-  goal_ccl : string;
-}
-
-type status = {
-  status_path : string option;
-  status_proofname : string option;
-}
+open Interface
 
-type goals =
-  | No_current_proof
-  | Proof_completed
-  | Unfocused_goals of goal list
-  | Uninstantiated_evars of string list
-  | Goals of goal list
-
-type hint = (string * string) list
+type xml = Xml_parser.xml
 
 type 'a 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).
@@ -71,58 +51,18 @@ val inloadpath : string -> bool call
     followed by enough pattern variables. *)
 val mkcases : string -> string list list call
 
-
-(** * Coq answers to CoqIde *)
-
-type location = (int * int) option (* start and end of the error *)
-
-type 'a value =
-  | Good of 'a
-  | Fail of (location * string)
-
-(** * The structure that coqtop should implement *)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  handle_exn : exn -> location * string;
-}
-
 val abstract_eval_call : handler -> 'a call -> 'a value
 
 (** * XML data marshalling *)
 
 exception Marshal_error
 
-val of_bool : bool -> xml
-val to_bool : xml -> bool
-
-val of_string : string -> xml
-val to_string : xml -> string
-
-val of_int : int -> xml
-val to_int : xml -> int
-
-val of_pair : ('a -> xml) -> ('b -> xml) -> ('a * 'b) -> xml
-val to_pair : (xml -> 'a) -> (xml -> 'b) -> xml -> ('a * 'b)
-
-val of_list : ('a -> xml) -> 'a list -> xml
-val to_list : (xml -> 'a) -> xml -> 'a list
-
 val of_value : ('a -> xml) -> 'a value -> xml
 val to_value : (xml -> 'a) -> xml -> 'a value
 
 val of_call : 'a call -> xml
 val to_call : xml -> 'a call
 
-val of_goals : goals -> xml
-val to_goals : xml -> goals
-
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : xml -> 'a value
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 60b89c2236..76cf15f798 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -14,7 +14,7 @@ open Pp
 open Printer
 open Namegen
 
-(** Ide_slave : an implementation of [Ide_intf], i.e. mainly an interp
+(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
     when the -ideslave option is passed to Coqtop. Currently CoqIDE is
     the only one using this mode, but we try here to be as generic as
@@ -412,7 +412,7 @@ let process_goal sigma g =
 (*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
   let hyps =
     List.rev (Environ.fold_named_context process_hyp env ~init: []) in
-  { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl }
+  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl }
 (*         hyps,(ccl,concl_next_tac sigma g)) *)
 
 let goals () =
@@ -426,15 +426,15 @@ let goals () =
       let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
       if bgoals = [] then
         let exl = Evarutil.non_instantiated sigma in
-        if exl = [] then Ide_intf.Proof_completed
+        if exl = [] then Interface.Proof_completed
         else
           let el = List.map (fun evar -> string_of_ppcmds (pr_evar evar)) exl in
-          Ide_intf.Uninstantiated_evars el
-      else Ide_intf.Unfocused_goals (List.map (process_goal sigma) bgoals)
+          Interface.Uninstantiated_evars el
+      else Interface.Unfocused_goals (List.map (process_goal sigma) bgoals)
     end
   else
-    Ide_intf.Goals (List.map (process_goal sigma) all_goals)
-  with Proof_global.NoCurrentProof -> Ide_intf.No_current_proof
+    Interface.Goals (List.map (process_goal sigma) all_goals)
+  with Proof_global.NoCurrentProof -> Interface.No_current_proof
 
 let hints () =
   try
@@ -470,7 +470,7 @@ let status () =
       Some (Names.string_of_id (Pfedit.get_current_proof_name ()))
     with _ -> None
   in
-  { Ide_intf.status_path = path; Ide_intf.status_proofname = proof }
+  { Interface.status_path = path; Interface.status_proofname = proof }
 
 (** Grouping all call handlers together + error handling *)
 
@@ -495,14 +495,14 @@ let eval_call c =
     r
   in
   let handler = {
-    Ide_intf.interp = interruptible interp;
-    Ide_intf.rewind = interruptible rewind;
-    Ide_intf.goals = interruptible goals;
-    Ide_intf.hints = interruptible hints;
-    Ide_intf.status = interruptible status;
-    Ide_intf.inloadpath = interruptible inloadpath;
-    Ide_intf.mkcases = interruptible Vernacentries.make_cases;
-    Ide_intf.handle_exn = handle_exn; }
+    Interface.interp = interruptible interp;
+    Interface.rewind = interruptible rewind;
+    Interface.goals = interruptible goals;
+    Interface.hints = interruptible hints;
+    Interface.status = interruptible status;
+    Interface.inloadpath = interruptible inloadpath;
+    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());
@@ -511,7 +511,7 @@ let eval_call c =
 
 (** The main loop *)
 
-(** Exceptions during eval_call should be converted into [Ide_intf.Fail]
+(** Exceptions during eval_call should be converted into [Interface.Fail]
     messages by [handle_exn] above. Otherwise, we die badly, after having
     tried to send a last message to the ide: trying to recover from errors
     with the current protocol would most probably bring desynchronisation
@@ -522,7 +522,7 @@ let pr_debug s =
   if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let fail err =
-  Ide_intf.of_value (fun _ -> assert false) (Ide_intf.Fail (None, err))
+  Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err))
 
 let loop () =
   let p = Xml_parser.make () in
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
new file mode 100644
index 0000000000..b08365e7a5
--- /dev/null
+++ b/toplevel/interface.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Declarative part of the interface of CoqIde calls to Coq *)
+
+(** * Generic structures *)
+
+type raw = bool
+type verbose = bool
+
+type goal = {
+  goal_hyp : string list;
+  goal_ccl : string;
+}
+
+type status = {
+  status_path : string option;
+  status_proofname : string option;
+}
+
+type goals =
+  | No_current_proof
+  | Proof_completed
+  | Unfocused_goals of goal list
+  | Uninstantiated_evars of string list
+  | Goals of goal list
+
+type hint = (string * string) list
+
+(** * Coq answers to CoqIde *)
+
+type location = (int * int) option (* start and end of the error *)
+
+type 'a value =
+  | Good of 'a
+  | Fail of (location * string)
+
+(** * The structure that coqtop should implement *)
+
+type handler = {
+  interp : raw * verbose * string -> string;
+  rewind : int -> int;
+  goals : unit -> goals;
+  hints : unit -> (hint list * hint) option;
+  status : unit -> status;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
+  handle_exn : exn -> location * string;
+}
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 8b03e93803..4df717e102 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,6 +18,7 @@ Mltop
 Vernacentries
 Whelp
 Vernac
+Interface
 Ide_intf
 Ide_slave
 Toplevel