Fabrication de l'uri a partir du path utilisateur

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

2 files changed, 30 insertions, 5 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 798b1ccb1..70aa0a291 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -125,11 +125,37 @@ let token_list_of_kernel_name ~keep_sections kn tag =
     [N.string_of_label label ^ "." ^ (ext_of_tag tag)]
 ;;
 
-let uri_of_kernel_name ?(keep_sections=false) kn tag =
+let token_list_of_path dir id tag =
+ let module N = Names in
+  let token_list_of_dirpath dirpath =
+   List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
+  token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
+
+let token_list_of_kernel_name ~keep_sections kn tag =
  let module N = Names in
+ let module LN = Libnames in
+ let dir = match tag with
+   | Variable -> if keep_sections then Lib.cwd () else N.empty_dirpath
+   | Constant -> 
+       let ref = LN.ConstRef kn in
+       if keep_sections then LN.dirpath (Nametab.sp_of_global ref)
+       else Lib.library_part ref
+   | Inductive ->
+       let ref = LN.IndRef (kn,0) in
+      if keep_sections then LN.dirpath(Nametab.sp_of_global ref)
+      else Lib.library_part ref
+ in
+ let id = N.id_of_label (N.label kn) in
+ token_list_of_path dir id tag
+;;
+
+let uri_of_kernel_name ?(keep_sections=false) kn tag =
   let tokens = token_list_of_kernel_name ~keep_sections kn tag in
    "cic:/" ^ String.concat "/" tokens
-;;
+
+let uri_of_path dir id tag =
+  let tokens = token_list_of_path dir id tag in
+   "cic:/" ^ String.concat "/" tokens
 
 (* Special functions for handling of CCorn's CProp "sort" *)
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 651b85b0c..b120a95bc 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -544,7 +544,7 @@ let show_pftreestate fn (kind,pftst) id =
  let kn = Lib.make_kn id in
  let env = Global.env () in
  let obj = mk_current_proof_obj id val0 typ evar_map env in
- let uri = Cic2acic.uri_of_kernel_name kn Cic2acic.Constant in
+ let uri = Cic2acic.uri_of_path (Lib.cwd()) id Cic2acic.Constant in
   print_object_kind uri (kind_of_goal kind);
   print_object uri obj evar_map
    (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,
@@ -553,8 +553,7 @@ let show_pftreestate fn (kind,pftst) id =
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
- let (_,kind,_,_) = Pfedit.current_proof_statement () in
- let id = Pfedit.get_current_proof_name () in
+ let (id,kind,_,_) = Pfedit.current_proof_statement () in
   show_pftreestate fn (kind,pftst) id
 ;;