X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryMisc.ml;h=fb32d8c2425fb49fbd59f254e855a7c790d2ccf7;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=bb5bb74aef24488ef686d449ca7db7fcc58de6fb;hpb=ab2b9e54afe3a66d7283e6205e63dd48a2733b73;p=helm.git diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml index bb5bb74ae..fb32d8c24 100644 --- a/helm/ocaml/mathql/mQueryMisc.ml +++ b/helm/ocaml/mathql/mQueryMisc.ml @@ -23,6 +23,17 @@ * http://cs.unibo.it/helm/. *) +(****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* Ferruccio Guidi *) +(* 15/01/2003 *) +(* *) +(* *) +(****************************************************************************) + exception IllFormedUri of string;; let string_of_cic_textual_parser_uri uri = @@ -43,7 +54,6 @@ let string_of_cic_textual_parser_uri uri = ;; let cic_textual_parser_uri_of_string uri' = - prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri'); try (* Constant *) if String.sub uri' (String.length uri' - 4) 4 = ".con" then @@ -72,10 +82,6 @@ let cic_textual_parser_uri_of_string uri' = | Invalid_argument _ -> raise (IllFormedUri uri') ;; -let cic_textual_parser_uri_of_string uri' = - let res = cic_textual_parser_uri_of_string uri' in - prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res)); - res (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) let wrong_xpointer_format_from_wrong_xpointer_format' uri = @@ -100,3 +106,15 @@ 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 ^ ")"