]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataPp.ml
removed no longer used METAs
[helm.git] / helm / ocaml / metadata / metadataPp.ml
index fdbbaf071f133afc377845f71ccfdbf844dce824..373ec540fcbab9576c14bb5e1504b23c128e3420 100644 (file)
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open MetadataTypes
@@ -71,8 +73,8 @@ type t = [ `Int of int | `String of string | `Null ]
 
 let columns_of_metadata_aux ~about metadata =
   let sort s = `String (CicPp.ppsort s) in
-  let source = `String about in
-  let occurrence u = `String u in
+  let source = `String (UriManager.string_of_uri about) in
+  let occurrence u = `String (UriManager.string_of_uri u) in
   List.fold_left
     (fun (sort_cols, rel_cols, obj_cols) metadata ->
       match metadata with
@@ -102,7 +104,7 @@ let pp_constr =
          (CicPp.ppsort sort) (String.concat ";" (List.map pp_position p))
     | `Rel p -> sprintf "Rel [%s]" (String.concat ";" (List.map pp_position p))
     | `Obj (uri, p) -> sprintf "Obj %s; [%s]" 
-       uri (String.concat ";" (List.map pp_position p))
+       (UriManager.string_of_uri uri) (String.concat ";" (List.map pp_position p))
  
 (*
 let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) =