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 32d8ae54da64d11ac23e7a0ce0b2fee899921911..7606344d1b1feea9981fd442e1228084f48ff7b1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -53,20 +53,22 @@ 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
 let _ =
   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
     [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with";
-    "in"; "and"; "to"; "as"; "on"]
+    "in"; "and"; "to"; "as"; "on"; "names"]
 
 let error lexbuf msg =
   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))