added syntax for URIs

[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 8a6faa19339fe2979b75b5407ebeca108f551ed6..b62230a335aa84b1da78e8d3eb0687b6c00b534a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -33,8 +33,10 @@ let regexp blank = [ ' ' '\t' '\n' ]
 let regexp paren = [ '(' '[' '{' ')' ']' '}' ]
 let regexp implicit = '?'
 let regexp symbol_char =
-  [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' '\\' '(' '[' '{' ')' ']' '}' ]
-
+  [^ 'a' - 'z' 'A' - 'Z' '0' - '9'
+     ' ' '\t' '\n'
+     '\\' '(' '[' '{' ')' ']' '}' '?'
+  ]
 let regexp blanks = blank+
 let regexp num = digit+
 let regexp tex_token = '\\' alpha+
@@ -46,8 +48,10 @@ let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+)
 let regexp meta = implicit num
 let regexp qstring = '"' [^ '"']* '"'
 let regexp uri =
-  (*      schema      *) (*     path     *) (*  ext   *) (*    xpointer     *)
-  ("cic:/" | "theory:/") ident ('/' ident)* ('.' ident)+ ('#' num ('/' num)*)?
+  ("cic:/" | "theory:/")              (* schema *)
+  ident ('/' ident)*                  (* path *)
+  ('.' ident)+                        (* ext *)
+  ("#xpointer(" num ('/' num)+ ")")?    (* xpointer *)
 (* let regexp catchall = .* *)
 
 let keywords = Hashtbl.create 17