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

5 files changed, 50 insertions, 50 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