]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryMisc.ml
ported to latest lablgtk2 snapshot
[helm.git] / helm / ocaml / mathql / mQueryMisc.ml
index 92805067971ef6699f03c58886a4cdc60c83abd0..fb32d8c2425fb49fbd59f254e855a7c790d2ccf7 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
+(****************************************************************************)
+(*                                                                          *)
+(*                               PROJECT HELM                               *)
+(*                                                                          *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>             *)
+(*                Ferruccio Guidi        <fguidi@cs.unibo.it>               *)
+(*                                 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 ^ ")"