]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
Ported to Http_registry and to HelmLogger.
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualLexer2.ml
index bcc8fda28486221bbafa1bbd17c65eac1de52cf9..71574dbb1ce081e24da3455739cedba56f70ba76 100644 (file)
@@ -35,7 +35,7 @@ let regexp blanks = blank+
 let regexp num = digit+
 let regexp tex_token = '\\' alpha+
 let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ]
-let regexp ident_cont = alpha | num | '_'
+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'+)
@@ -111,8 +111,8 @@ let rec token = lexer
         Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
       in
       (try
-        return lexbuf ("SYMBOL", Macro.expand macro)
-      with Macro.Macro_not_found _ ->
+        return lexbuf ("SYMBOL", CicTextualParser2Macro.expand macro)
+      with CicTextualParser2Macro.Macro_not_found _ ->
         return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf))
   | eof -> return lexbuf ("EOI", "")
   | _ -> error lexbuf "Invalid character"