diff options
-rw-r--r-- | toplevel/ide_intf.mli | 2 | ||||
-rw-r--r-- | toplevel/ide_slave.ml | 21 | ||||
-rw-r--r-- | toplevel/usage.ml | 2 |
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\ |