Porting to the new "long-identifiers" editex lexer.

[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 25fc01311bdbd7031269179e4958ab46ecb47f78..01ddd0cf302acdede1f9b14f086864077677ce10 100644 (file)
--- 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 "_" *)
@@ -55,14 +63,15 @@
 }
 let dollar = '$'
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-'] | "\\_"
-let ident = alfa (alfa | num)*
+let letter = ['A'-'Z' 'a'-'z']
+let alfa = letter | ['_' ''' '-'] | "\\_"
+let ident = letter (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
 let conuri = baseuri "con"
 let varuri = baseuri "var"
 let indtyuri = baseuri "ind#1/" num
 let indconuri = baseuri "ind#1/" num "/" num
-let blanks = [' ' '\t' '\n' '~' '{' '}'] | "\\;"
+let blanks = [' ' '\t' '\n' '~' '{' '}'] | "\\;" | "\\rm"
 rule token =
  parse
     blanks      { token lexbuf } (* skip blanks *)
@@ -107,6 +116,7 @@ rule token =
   | eof         { EOF }
   (* Arithmetical operators *)
   | '+'         { PLUS }
+  | '-'         { MINUS }
   | '*'         { TIMES }
   | '='         { EQ }
 {}