diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-16 11:33:05 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-16 11:33:05 +0000 |
commit | 60618d500c2d32c8e85e599022ceb8cff2a220a3 (patch) | |
tree | bf13371812d448db4d07d88b00ef6e9b7855b6d6 /tools/coqdoc/cpretty.mll | |
parent | a6d740dd7fcf43202b223b6a88adfe0d8884a3c6 (diff) |
Fix handling of space after "Notation" or "where", add missing keywords.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 43a4b0eb9..925f5258c 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -510,7 +510,7 @@ rule coq_bol = parse output_indented_keyword s lexbuf; let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space* notation_kw space* + | space* notation_kw { let s = lexeme lexbuf in output_indented_keyword s lexbuf; let eol= start_notation_string lexbuf in @@ -637,7 +637,7 @@ and coq = parse Output.ident s (lexeme_start lexbuf); let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | notation_kw space* + | notation_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); let eol= start_notation_string lexbuf in @@ -1102,7 +1102,7 @@ and body = parse if eol then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end else body lexbuf } - | "where" space* + | "where" { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) (lexeme_start lexbuf); start_notation_string lexbuf } @@ -1126,6 +1126,8 @@ and body = parse body lexbuf } and start_notation_string = parse + | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0); + start_notation_string lexbuf } | '"' (* a true notation *) { Output.sublexer '"' (lexeme_start lexbuf); notation_string lexbuf; |