moved string_of_uriref from MQueryMisc to UriManager

diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml
index fb32d8c2425fb49fbd59f254e855a7c790d2ccf7..08474d3947aac3b2d6220ab61edae443bebf8e14 100644 (file)
--- a/helm/ocaml/mathql/mQueryMisc.ml
+++ b/helm/ocaml/mathql/mQueryMisc.ml
@@ -106,15 +106,3 @@ let term_of_cic_textual_parser_uri uri =
    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 ;;
 
-(* conversion functions *****************************************************)
-
-type uriref = UriManager.uri * (int list)
-
-let string_of_uriref (uri, fi) =
-   let module UM = UriManager in
-   let str = UM.string_of_uri uri in
-   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
-   match fi with
-      | []          -> str 
-      | [t]         -> str ^ xp t ^ ")" 
-      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 

diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli
index 6fb600dab35417f4d9ca5d343fed83abce122b5a..57c24d1897b617d3bee76c9894fddf05a1e471d3 100644 (file)
--- a/helm/ocaml/mathql/mQueryMisc.mli
+++ b/helm/ocaml/mathql/mQueryMisc.mli
@@ -41,6 +41,3 @@ val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
 val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term
 val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
 
-type uriref = UriManager.uri * (int list)
-
-val string_of_uriref : uriref -> string

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 39d058b5e54c0f749a7606150f6ddfc004eb7d73..3028cf2b9b37e5d527bf35e6d89a07ed23ea7f72 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -138,3 +138,14 @@ let innertypesuri_of_uri uri =
    newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
    newuri
 ;;
+
+type uriref = uri * (int list)
+
+let string_of_uriref (uri, fi) =
+   let str = string_of_uri uri in
+   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
+   match fi with
+      | []          -> str 
+      | [t]         -> str ^ xp t ^ ")" 
+      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
+

diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 0f4f15ea2822ce998847a7312759a7352dfb397f..703b0b4f1629e12639d64767a2c825b274fb49c8 100644 (file)
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -53,3 +53,15 @@ val bodyuri_of_uri : uri -> uri option
 
 (* given an uri, it gives back the uri of its inner types             *)
 val innertypesuri_of_uri : uri -> uri
+
+(*
+val mutind_uri:       uri -> int -> uri
+val mutconstruct_uri: uri -> int -> int -> uri
+val mutind:           uri -> uri * int
+val mutconstruct:     uri -> uri * int * int
+*)
+
+  (* builder for MutInd and MutConstruct URIs *)
+type uriref = uri * (int list)
+val string_of_uriref : uriref -> string
+