X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=f2d083063258da907818ec93939309a44712a302;hb=d423e5e29035b1dfdc87ae2ff201b0584456e751;hp=617c10fe6f45aa372eef945ddfc80c8cc29fccd8;hpb=6afdc65fcdb592dccb751849f65b1f482ef97cd6;p=goals.git

diff --git a/src/lexer.mll b/src/lexer.mll
index 617c10f..f2d0830 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -34,7 +34,7 @@ let new_line lexbuf =
 let white = [' ' '\t']+
 let newline = '\r' | '\n' | "\r\n"
 let comment = '#' (_#'\n')*
-let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
+let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']*
 
 rule read =
     parse
@@ -43,6 +43,7 @@ rule read =
     | newline { new_line lexbuf; read lexbuf }
     | ","     { COMMA }
     | ":"     { COLON }
+    | ";"     { SEMICOLON }
     | "="     { EQUALS }
     | "("     { LEFT_PAREN }
     | ")"     { RIGHT_PAREN }
@@ -54,6 +55,7 @@ rule read =
     | "tactic" { TACTIC_KEYWORD }
     | "let"   { LET }
     | "include" { INCLUDE }
+    | "-include" { OPTINCLUDE }
     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
@@ -106,7 +108,8 @@ and read_string buf =
  *)
 and read_code buf level =
     parse
-    | '{'     { incr level; read_code buf level lexbuf }
+    | '{'     { Ast.Substs.add_char buf '{';
+                incr level; read_code buf level lexbuf }
     | '}'     { decr level;
                 if !level = 0 then CODE (Ast.Substs.get buf)
                 else (