X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=2b6c4e8020f9afa321d21e8b290ac746e73c0614;hb=e23952e03c37201fe805ad3d1635e7d2d41e5908;hp=66c6b9feef221ef2b0d22b58c5a52123222ed972;hpb=976bb1b35d77f3058df3c25c1e2a4767147d606b;p=goals.git

diff --git a/src/lexer.mll b/src/lexer.mll
index 66c6b9f..2b6c4e8 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -28,7 +28,7 @@ exception SyntaxError of string
 let new_line lexbuf =
   let pos = lexbuf.lex_curr_p in
   lexbuf.lex_curr_p <-
-    { pos with pos_bol = lexbuf.lex_curr_pos; pos_lnum = pos.pos_lnum + 1 }
+    { pos with pos_bol = pos.pos_cnum; pos_lnum = pos.pos_lnum + 1 }
 }
 
 let white = [' ' '\t']+
@@ -50,17 +50,27 @@ rule read =
     | "["     { LEFT_ARRAY }
     | "]"     { RIGHT_ARRAY }
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
-    | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
+    | "{"     { read_code false (Ast.Substs.create ()) (ref 1) lexbuf }
+    | "@{"    { read_code true  (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
     | "tactic"
               { TACTIC_KEYWORD }
     | "function"
               { FUNCTION }
+    | "pure"  { PURE }
     | "let"   { LET }
     | "include"
               { INCLUDE }
     | "-include"
               { OPTINCLUDE }
+    | "returning"
+              { RETURNING }
+    | "expression"
+              { EXPRESSION }
+    | "string"
+              { STRING_KEYWORD }
+    | "strings"
+              { STRINGS }
     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
@@ -111,31 +121,31 @@ and read_string buf =
  * Note the range of %-substitutions possible is larger than
  * for strings.
  *)
-and read_code buf level =
+and read_code quiet buf level =
     parse
     | '{'     { Ast.Substs.add_char buf '{';
-                incr level; read_code buf level lexbuf }
+                incr level; read_code quiet buf level lexbuf }
     | '}'     { decr level;
-                if !level = 0 then CODE (Ast.Substs.get buf)
+                if !level = 0 then CODE (Ast.Substs.get buf, quiet)
                 else (
                   Ast.Substs.add_char buf '}';
-                  read_code buf level lexbuf
+                  read_code quiet buf level lexbuf
                 ) }
     | newline { Ast.Substs.add_char buf '\n';
-                new_line lexbuf; read_code buf level lexbuf }
-    | '%' '%' { Ast.Substs.add_char buf '%'; read_code buf level lexbuf }
-    | '%' '@' { Ast.Substs.add_var buf "@"; read_code buf level lexbuf }
-    | '%' '<' { Ast.Substs.add_var buf "<"; read_code buf level lexbuf }
-    | '%' '^' { Ast.Substs.add_var buf "^"; read_code buf level lexbuf }
+                new_line lexbuf; read_code quiet buf level lexbuf }
+    | '%' '%' { Ast.Substs.add_char buf '%'; read_code quiet buf level lexbuf }
+    | '%' '@' { Ast.Substs.add_var buf "@"; read_code quiet buf level lexbuf }
+    | '%' '<' { Ast.Substs.add_var buf "<"; read_code quiet buf level lexbuf }
+    | '%' '^' { Ast.Substs.add_var buf "^"; read_code quiet buf level lexbuf }
     | '%' id  { let id = Lexing.lexeme lexbuf in
                 let len = String.length id in
                 Ast.Substs.add_var buf (String.sub id 1 (len-1));
-                read_code buf level lexbuf }
+                read_code quiet buf level lexbuf }
     | '%' _   { raise (SyntaxError ("illegal character in %-substitution: " ^
                                       Lexing.lexeme lexbuf)) }
     | [^ '{' '}' '\r' '\n' '%' ]+
               { Ast.Substs.add_string buf (Lexing.lexeme lexbuf);
-                read_code buf level lexbuf }
+                read_code quiet buf level lexbuf }
     | _       { raise (SyntaxError ("illegal character in code section: " ^
                                       Lexing.lexeme lexbuf)) }
     | eof     { raise (SyntaxError ("unterminated code section")) }