X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualLexer.mll;h=7f70b8e880989066536a7a4a21453df65c4da77f;hb=87218276a42635aad90a91757d431a9cb61983a4;hp=25fc01311bdbd7031269179e4958ab46ecb47f78;hpb=a537ad12d57d10498d9b572290f6050dece06b0a;p=helm.git

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 25fc01311..7f70b8e88 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -31,21 +31,29 @@
  let indtyuri_of_uri uri =
   let index_sharp =  String.index uri '#' in
   let index_num = index_sharp + 3 in
-   (UriManager.uri_of_string (String.sub uri 0 index_sharp),
-    int_of_string (String.sub uri index_num (String.length uri - index_num)) - 1
-   )
+   try
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+     int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1
+    )
+   with
+    Failure msg ->
+     raise (CicTextualParser0.LexerFailure "Not an inductive URI")
  ;;
 
  let indconuri_of_uri uri =
   let index_sharp =  String.index uri '#' in
   let index_div = String.rindex uri '/' in
   let index_con = index_div + 1 in
-   (UriManager.uri_of_string (String.sub uri 0 index_sharp),
-    int_of_string
-     (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
-    int_of_string
-     (String.sub uri index_con (String.length uri - index_con))
-   )
+   try
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+     int_of_string
+      (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
+     int_of_string
+      (String.sub uri index_con (String.length uri - index_con))
+    )
+   with
+    Failure msg ->
+     raise (CicTextualParser0.LexerFailure "Not a constructor URI")
  ;;
 
  (* TeX unquoting for "_" *)