diff options
author | 2002-04-04 15:54:46 +0000 | |
---|---|---|
committer | 2002-04-04 15:54:46 +0000 | |
commit | 6bd6ed58860e7713fdf4aaaad2dabff204ae6646 (patch) | |
tree | fb883021c8416c2d0b21ff100473515d97107431 /tools/gallina_lexer.mll | |
parent | 25b5744b21394aebadcf4cf4a557c27c5e84db93 (diff) |
meilleure gestion du point terminal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2611 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/gallina_lexer.mll')
-rw-r--r-- | tools/gallina_lexer.mll | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index 98c838ed7..4d05688c3 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -23,6 +23,7 @@ } let space = [' ' '\t' '\n'] +let enddot = '.' (' ' | '\t' | '\n' | eof) rule action = parse | "Theorem" space { print "Theorem "; body lexbuf; @@ -78,26 +79,27 @@ and body_def = parse | _ { print (Lexing.lexeme lexbuf); body lexbuf } and body = parse - | '.' { print ".\n"; skip_proof lexbuf } - | ":=" { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body lexbuf } + | enddot { print ".\n"; skip_proof lexbuf } + | ":=" { print ".\n"; skip_proof lexbuf } + | "(*" { print "(*"; comment_depth := 1; + comment lexbuf; body lexbuf } + | eof { raise Fin_fichier } + | _ { print (Lexing.lexeme lexbuf); body lexbuf } and body_pgm = parse - | '.' { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body_pgm lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf } + | enddot { print ".\n"; skip_proof lexbuf } + | "(*" { print "(*"; comment_depth := 1; + comment lexbuf; body_pgm lexbuf } + | eof { raise Fin_fichier } + | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf } and skip_until_point = parse - | '.' { end_of_line lexbuf } - | "(*" { comment_depth := 1; - skip_comment lexbuf; skip_until_point lexbuf } - | eof { raise Fin_fichier } - | _ { skip_until_point lexbuf } + | '.' '\n' { () } + | enddot { end_of_line lexbuf } + | "(*" { comment_depth := 1; + skip_comment lexbuf; skip_until_point lexbuf } + | eof { raise Fin_fichier } + | _ { skip_until_point lexbuf } and end_of_line = parse | [' ' '\t' ]* { end_of_line lexbuf } @@ -119,7 +121,7 @@ and skip_proof = parse | "Abort" space { skip_until_point lexbuf } | "Proof" space { skip_until_point lexbuf } - | "Proof" [' ' '\t' ]* '.' { skip_proof lexbuf } + | "Proof" [' ' '\t']* '.' { skip_proof lexbuf } | "(*" { comment_depth := 1; skip_comment lexbuf; skip_proof lexbuf } | eof { raise Fin_fichier } |