From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 15 Oct 2004 14:08:00 +0000 (+0000)
Subject: moved string_of_uriref from MQueryMisc to UriManager
X-Git-Tag: V_0_0_10~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c63adaf9bd7a10eb9f7450528d7895115ee533e;p=helm.git

moved string_of_uriref from MQueryMisc to UriManager
---

diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml
index fb32d8c24..08474d394 100644
--- 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 6fb600dab..57c24d189 100644
--- 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 39d058b5e..3028cf2b9 100644
--- 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 0f4f15ea2..703b0b4f1 100644
--- 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
+