]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryMisc.ml
When the stylesheet from TML to MathML generated a document without a root
[helm.git] / helm / ocaml / mathql / mQueryMisc.ml
index 311596baa3e4523af9d1a2f4fed6ca91f00b1227..92805067971ef6699f03c58886a4cdc60c83abd0 100644 (file)
@@ -57,15 +57,20 @@ let cic_textual_parser_uri_of_string uri' =
       let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
        CicTextualParser0.IndTyUri (uri'',typeno)
      with
-      _ ->
-       (* Constructor of an Inductive Type *)
-       let uri'',typeno,consno =
-        CicTextualLexer.indconuri_of_uri uri'
-       in
-        CicTextualParser0.IndConUri (uri'',typeno,consno)
+        UriManager.IllFormedUri _
+      | CicTextualParser0.LexerFailure _
+      | Invalid_argument _ ->
+         (* Constructor of an Inductive Type *)
+         let uri'',typeno,consno =
+          CicTextualLexer.indconuri_of_uri uri'
+         in
+          CicTextualParser0.IndConUri (uri'',typeno,consno)
     )
  with
-  _ -> raise (IllFormedUri uri')
+    UriManager.IllFormedUri _
+  | CicTextualParser0.LexerFailure _
+  | Invalid_argument _ ->
+     raise (IllFormedUri uri')
 ;;
 let cic_textual_parser_uri_of_string uri' =
   let res = cic_textual_parser_uri_of_string uri' in
@@ -95,3 +100,14 @@ let term_of_cic_textual_parser_uri uri =
    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 ;;
 
+(* time handling  ***********************************************************)
+
+type time = float * float 
+
+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)