From eaca4fb2918eb1a1dd74409546d947f9353ed078 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 2 Feb 2012 17:15:55 +0000 Subject: 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 --- toplevel/ide_slave.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'toplevel/ide_slave.ml') diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 42ecb75bc..84aa98ea8 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 -- cgit v1.2.3