git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Implement tactics.
[goals.git]
/
src
/
lexer.mll
diff --git
a/src/lexer.mll
b/src/lexer.mll
index
a9b11d1
..
273b09d
100644
(file)
--- a/
src/lexer.mll
+++ b/
src/lexer.mll
@@
-51,10
+51,10
@@
rule read =
| '"' { read_string (Ast.Substs.create ()) lexbuf }
| "{" { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
| "goal" { GOAL }
| '"' { read_string (Ast.Substs.create ()) lexbuf }
| "{" { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
| "goal" { GOAL }
+ | "tactic" { TACTIC_KEYWORD }
| "let" { LET }
| "let" { LET }
- | "*" id { let id = Lexing.lexeme lexbuf in
- let len = String.length id in
- TACTIC (String.sub id 1 (len-1)) }
+ | "*" id { (* NB: The initial '*' is part of the name. *)
+ TACTIC (Lexing.lexeme lexbuf) }
| id { ID (Lexing.lexeme lexbuf) }
| _ { raise (SyntaxError ("unexpected character: " ^
Lexing.lexeme lexbuf)) }
| id { ID (Lexing.lexeme lexbuf) }
| _ { raise (SyntaxError ("unexpected character: " ^
Lexing.lexeme lexbuf)) }