From 9c63adaf9bd7a10eb9f7450528d7895115ee533e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 15 Oct 2004 14:08:00 +0000 Subject: [PATCH] moved string_of_uriref from MQueryMisc to UriManager --- helm/ocaml/mathql/mQueryMisc.ml | 12 ------------ helm/ocaml/mathql/mQueryMisc.mli | 3 --- helm/ocaml/urimanager/uriManager.ml | 11 +++++++++++ helm/ocaml/urimanager/uriManager.mli | 12 ++++++++++++ 4 files changed, 23 insertions(+), 15 deletions(-) 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 + -- 2.39.2