More information returned by coqtop about its internal state. Hopefully we'll manage to get rid of the own stack of coqide.

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

4 files changed, 41 insertions, 16 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 009a198920..2f53fa8ff3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2192,8 +2192,8 @@ let main files =
           "Oops, problem while fetching coq status."
         | Interface.Good status ->
           let path = match status.Interface.status_path with
-          | None -> ""
-          | Some p -> " in " ^ p
+          | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+          | _ :: l -> " in " ^ String.concat "." l
           in
           let name = match status.Interface.status_proofname with
           | None -> ""
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index fc8ffa2557..d36e466240 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -255,13 +255,25 @@ let to_call = function
 
 let of_status s =
   let of_so = of_option of_string in
-  Element ("status", [], [of_so s.status_path; of_so s.status_proofname])
+  let of_sl = of_list of_string in
+  Element ("status", [],
+    [
+      of_sl s.status_path;
+      of_so s.status_proofname;
+      of_sl s.status_allproofs;
+      of_int s.status_statenum;
+      of_int s.status_proofnum;
+    ]
+  )
 
 let to_status = function
-| Element ("status", [], [path; name]) ->
+| Element ("status", [], [path; name; prfs; snum; pnum]) ->
   {
-    status_path = to_option to_string path;
+    status_path = to_list to_string path;
     status_proofname = to_option to_string name;
+    status_allproofs = to_list to_string prfs;
+    status_statenum = to_int snum;
+    status_proofnum = to_int pnum;
   }
 | _ -> raise Marshal_error
 
@@ -385,9 +397,9 @@ let pr_string s = "["^s^"]"
 let pr_bool b = if b then "true" else "false"
 
 let pr_status s =
-  let path = match s.status_path with
-  | None -> "no path; "
-  | Some p -> "path = " ^ p ^ "; "
+  let path =
+    let l = String.concat "." s.status_path in
+    "path=" ^ l ^ ";"
   in
   let name = match s.status_proofname with
   | None -> "no proof;"
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 42ecb75bcb..84aa98ea80 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -461,16 +461,23 @@ let status () =
       and display the other parts (opened sections and modules) *)
   let path =
     let l = Names.repr_dirpath (Lib.cwd ()) in
-    let l = snd (Util.list_sep_last l) in
-    if l = [] then None
-    else Some (Names.string_of_dirpath (Names.make_dirpath l))
+    List.rev_map Names.string_of_id l
   in
   let proof =
-    try
-      Some (Names.string_of_id (Pfedit.get_current_proof_name ()))
+    try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
     with _ -> None
   in
-  { Interface.status_path = path; Interface.status_proofname = proof }
+  let allproofs =
+    let l = Proof_global.get_all_proof_names () in
+    List.map Names.string_of_id l
+  in
+  {
+    Interface.status_path = path;
+    Interface.status_proofname = proof;
+    Interface.status_allproofs = allproofs;
+    Interface.status_statenum = Lib.current_command_label ();
+    Interface.status_proofnum = Pfedit.current_proof_depth ();
+  }
 
 let get_options () =
   let table = Goptions.get_tables () in
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index e1410f5bc9..6040605504 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.mli
@@ -27,10 +27,16 @@ type evar = {
 }
 
 type status = {
-  status_path : string option;
+  status_path : string list;
   (** Module path of the current proof *)
   status_proofname : string option;
-  (** Current proof name. [None] if no proof is in progress *)
+  (** Current proof name. [None] if no focussed proof is in progress *)
+  status_allproofs : string list;
+  (** List of all pending proofs. Order is not significant *)
+  status_statenum : int;
+  (** A unique id describing the state of coqtop *)
+  status_proofnum : int;
+  (** An id describing the state of the current proof. *)
 }
 
 type goals = {