X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryMisc.ml;h=fb32d8c2425fb49fbd59f254e855a7c790d2ccf7;hb=fde0ad77237a2fbdfb5621d5b5085fe7c82e3f92;hp=92805067971ef6699f03c58886a4cdc60c83abd0;hpb=03dee221bd1f2c9a6e7f74d9abf88be14aac7763;p=helm.git diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml index 928050679..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,14 +106,15 @@ let term_of_cic_textual_parser_uri uri = | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) ;; -(* time handling ***********************************************************) +(* conversion functions *****************************************************) -type time = float * float +type uriref = UriManager.uri * (int list) -let start_time () = - (Sys.time (), Unix.time ()) - -let stop_time (s0, u0) = - let s1 = Sys.time () in - let u1 = Unix.time () in - Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) +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 ^ ")"