Added an interface primitive to ask coqtop for its internal versions.

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

4 files changed, 54 insertions, 0 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 52b5dbb7cb..02ca25a9de 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -70,6 +70,13 @@ type option_state = {
   (** The current value of the option *)
 }
 
+type coq_info = {
+  coqtop_version : string;
+  protocol_version : string;
+  release_date : string;
+  compile_date : string;
+}
+
 (** * Coq answers to CoqIde *)
 
 type location = (int * int) option (* start and end of the error *)
diff --git a/lib/serialize.ml b/lib/serialize.ml
index a793e800eb..8d677ffbf1 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -6,6 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Protocol version of this file. This is the date of the last modification. *)
+
+(** WARNING: TO BE UPDATED WHEN MODIFIED! *)
+
+let protocol_version = "20120511"
+
 (** * Interface of calls to Coq by CoqIde *)
 
 open Interface
@@ -28,6 +34,7 @@ type 'a call =
   | InLoadPath of string
   | MkCases of string
   | Quit
+  | About
 
 (** The structure that coqtop should implement *)
 
@@ -43,6 +50,7 @@ type handler = {
   inloadpath : string -> bool;
   mkcases : string -> string list list;
   quit : unit -> unit;
+  about : unit -> coq_info;
   handle_exn : exn -> location * string;
 }
 
@@ -76,6 +84,7 @@ let abstract_eval_call handler c =
       | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
       | MkCases s -> Obj.magic (handler.mkcases s : string list list)
       | Quit -> Obj.magic (handler.quit () : unit)
+      | About -> Obj.magic (handler.about () : coq_info)
     in Good res
   with e ->
     let (l, str) = handler.handle_exn e in
@@ -250,6 +259,8 @@ let of_call = function
   Element ("call", ["val", "mkcases"], [PCData ind])
 | Quit ->
   Element ("call", ["val", "quit"], [])
+| About ->
+  Element ("call", ["val", "about"], [])
 
 let to_call = function
 | Element ("call", attrs, l) ->
@@ -273,6 +284,7 @@ let to_call = function
   | "mkcases" -> MkCases (raw_string l)
   | "hints" -> Hints
   | "quit" -> Quit
+  | "about" -> About
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -334,6 +346,23 @@ let to_goals = function
   { fg_goals = fg; bg_goals = bg; }
 | _ -> raise Marshal_error
 
+let of_coq_info info =
+  let version = of_string info.coqtop_version in
+  let protocol = of_string info.protocol_version in
+  let release = of_string info.release_date in
+  let compile = of_string info.compile_date in
+  Element ("coq_info", [], [version; protocol; release; compile])
+
+let to_coq_info = function
+| Element ("coq_info", [], [version; protocol; release; compile]) ->
+  {
+    coqtop_version = to_string version;
+    protocol_version = to_string protocol;
+    release_date = to_string release;
+    compile_date = to_string compile;
+  }
+| _ -> raise Marshal_error
+
 let of_hints =
   let of_hint = of_list (of_pair of_string of_string) in
   of_option (of_pair (of_list of_hint) of_hint)
@@ -351,6 +380,7 @@ let of_answer (q : 'a call) (r : 'a value) =
   | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
   | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
   | Quit -> Obj.magic (fun _ -> Element ("unit", [], []))
+  | About -> Obj.magic (of_coq_info : coq_info -> xml)
   in
   of_value convert r
 
@@ -370,6 +400,7 @@ let to_answer xml =
     | "evar" -> Obj.magic (to_evar elt : evar)
     | "option_value" -> Obj.magic (to_option_value elt : option_value)
     | "option_state" -> Obj.magic (to_option_state elt : option_state)
+    | "coq_info" -> Obj.magic (to_coq_info elt : coq_info)
     | _ -> raise Marshal_error
     end
   | _ -> raise Marshal_error
@@ -414,6 +445,7 @@ let pr_call = function
   | InLoadPath s -> "INLOADPATH "^s
   | MkCases s -> "MKCASES "^s
   | Quit -> "QUIT"
+  | About -> "ABOUT"
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
@@ -473,3 +505,5 @@ let pr_full_value call value =
     | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
     | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
     | Quit -> pr_value value
+    | About -> pr_value value
+
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 6407276bae..112472d4e3 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -84,11 +84,16 @@ type handler = {
   inloadpath : string -> bool;
   mkcases : string -> string list list;
   quit : unit -> unit;
+  about : unit -> coq_info;
   handle_exn : exn -> location * string;
 }
 
 val abstract_eval_call : handler -> 'a call -> 'a value
 
+(** * Protocol version *)
+
+val protocol_version : string
+
 (** * XML data marshalling *)
 
 exception Marshal_error
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index b4a2178245..ba8463515e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -261,6 +261,13 @@ let set_options options =
   in
   List.iter iter options
 
+let about () = {
+  Interface.coqtop_version = Coq_config.version;
+  Interface.protocol_version = Serialize.protocol_version;
+  Interface.release_date = Coq_config.date;
+  Interface.compile_date = Coq_config.compile_date;
+}
+
 (** Grouping all call handlers together + error handling *)
 
 exception Quit
@@ -306,6 +313,7 @@ let eval_call c =
     Serialize.set_options = interruptible set_options;
     Serialize.mkcases = interruptible Vernacentries.make_cases;
     Serialize.quit = (fun () -> raise Quit);
+    Serialize.about = interruptible about;
     Serialize.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)