Ide_slave: a more robust current_status () function

 - Due to -top foobar, or -notop, the current dir_path () doesn't
   necessary starts by Top.
 - Start documenting Ide_intf

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

3 files changed, 18 insertions, 7 deletions

diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 42d1a943a..9d58ae033 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -21,8 +21,10 @@ val interp : bool -> string -> int call
 val rewind : int -> int 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" *)
 val current_status : string call
 val current_goals : goals call
+(** What has been displayed by coqtop recently ? *)
 val read_stdout : string call
 
 (** * Coq answers to CoqIde *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 0c9a1e79d..26279c53b 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -462,11 +462,21 @@ let make_cases s =
     | _ -> raise Not_found
 
 let current_status () =
-  let path = string_of_ppcmds (Libnames.pr_dirpath (Lib.cwd ())) in
-  let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
-  try
-    path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
-  with _ -> path
+  (** We remove the initial part of the current [dir_path]
+      (usually Top in an interactive session, cf "coqtop -top"),
+      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 "" else
+      (" in "^Names.string_of_dirpath (Names.make_dirpath l))
+  in
+  let proof =
+    try
+      ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
+    with _ -> ""
+  in
+  "Ready"^path^proof
 
 let orig_stdout = ref stdout
 
@@ -489,7 +499,6 @@ let init_stdout,read_stdout =
              let r = Buffer.contents out_buff in
              Buffer.clear out_buff; r)
 
-(* XXX - duplicates toplevel/toplevel.ml. should be merged. *)
 let explain_exn e =
   let toploc,exc =
     match e with
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 34e8d0fb5..84e38c0a1 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -24,7 +24,7 @@ let print_usage_channel co command =
 \n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
 \n  -R dir coqdir          (idem)\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
-\n  -notop    r            set the toplevel name to be the empty logical path\
+\n  -notop                 set the toplevel name to be the empty logical path\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
 \n  -inputstate f          read state from file f.coq\