The two lexers now raise CicTextualParser0.LexerFailure instead of

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualLexer.mll

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 692a6a86b1f6e0a47e087e720c52d5b5cb4b0dfe..7f70b8e880989066536a7a4a21453df65c4da77f 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -31,21 +31,34 @@
  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 "_" *)
+ let unquote str =
+  Str.global_replace (Str.regexp "\\\\_") "_" str
  ;;
 }
 let dollar = '$'
@@ -67,11 +80,15 @@ rule token =
   | "\\Set"     { SET }
   | "\\Prop"    { PROP }
   | "\\Type"    { TYPE }
-  | ident       { ID (L.lexeme lexbuf) }
-  | conuri      { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
-  | varuri      { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
-  | indtyuri    { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) }
-  | indconuri   { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) }
+  | ident       { ID (unquote (L.lexeme lexbuf)) }
+  | conuri      { CONURI
+                   (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | varuri      { VARURI
+                   (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | indtyuri    { INDTYURI
+                   (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | indconuri   { INDCONURI
+                   (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
   | '?' num     { let lexeme = L.lexeme lexbuf in
                    META