version 0.7.1

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualLexer2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 92a24ec8278b2d50dcb26598b3e81f4d17878160..7606344d1b1feea9981fd442e1228084f48ff7b1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -53,13 +53,15 @@ let regexp ident_cont = alpha | num | '_' | '\''
 let regexp ident_cont' = ident_cont | tex_token
 let regexp ident = (alpha ident_cont*) | ('_' ident_cont+)
 let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+)
+let regexp uri_step = (alpha (ident_cont|'-')*)
 let regexp meta = implicit num
 let regexp qstring = '"' [^ '"']* '"'
+let regexp uri_suffix = "con"|"ind"|"var"
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
-  ident ('/' ident)*                  (* path *)
-  ('.' ident)+                        (* ext *)
-  ("#xpointer(" num ('/' num)+ ")")?    (* xpointer *)
+  uri_step ('/' uri_step)*            (* path *)
+  ('.' uri_suffix)+                   (* ext *)
+  ("#xpointer(" num ('/' num)+ ")")?  (* xpointer *)
 (* let regexp catchall = .* *)
 
 let keywords = Hashtbl.create 17