snapshot (first working implementation of parttern matching from level 2

[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 8ad805c8dd36187be0ad0a1d4e86bfbe8f647104..3c262ceec1854c27a502b9c56f1d8853a04bd430 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -43,6 +43,8 @@ let regexp keyword = '"' ident '"'
 let regexp implicit = '?'
 let regexp meta = implicit number
 
+let regexp csymbol = '\'' ident
+
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
   ident ('/' ident)*                  (* path *)
@@ -114,6 +116,7 @@ let rec token = lexer
   | tex_token -> return lexbuf (expand_macro lexbuf)
   | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
   | eof -> return lexbuf ("EOI", "")
+  | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
   | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
 
 (* API implementation *)