snapshot, notably:

[helm.git] / helm / ocaml / cic_notation / cicNotationLexer.ml

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 306cf45b915f88d324ebed695b90ec0caaeb367c..9721ee80503e22af6e4499a334ed6e8cf312784a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -40,6 +40,12 @@ let regexp keyword = '"' ident '"'
 let regexp implicit = '?'
 let regexp meta = implicit number
 
+let regexp uri =
+  ("cic:/" | "theory:/")              (* schema *)
+  ident ('/' ident)*                  (* path *)
+  ('.' ident)+                        (* ext *)
+  ("#xpointer(" number ('/' number)+ ")")?  (* xpointer *)
+
 let error lexbuf msg =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
   raise (Error (begin_cnum, end_cnum, msg))
@@ -105,13 +111,14 @@ let rec level1_token = lexer
 (** {2 Level 2 lexer} *)
 
 let rec level2_token = lexer
-  | xml_blank+ -> level1_token lexbuf
+  | xml_blank+ -> level2_token lexbuf
   | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
   | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
   | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
   | keyword -> return lexbuf (keyword lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
+  | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
   | eof -> return lexbuf ("EOI", "")
   | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)