aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-06 11:49:35 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-06 11:49:35 +0000
commit76c0b528f625d5f5515dc331f938317904794cf4 (patch)
tree1a0d1ef83f3bd47535ea8dc5d08586552fa1e678 /tools/coqdoc
parent6a48116253b983c8f1f1735ea56199c2c9124314 (diff)
Petite modification de la gestion du '.' (jmn)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/pretty.mll7
1 files changed, 3 insertions, 4 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 0cf9249f0..29119e3f8 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -201,8 +201,6 @@
let space = [' ' '\t']
let space_nl = [' ' '\t' '\n' '\r']
-let enddot = '.' space_nl
-
let firstchar =
['A'-'Z' 'a'-'z' '_'
(* iso 8859-1 accents *)
@@ -499,13 +497,14 @@ and skip_proof = parse
| "(*" { ignore (comment lexbuf); skip_proof lexbuf }
| "Save" | "Qed" | "Defined"
| "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf }
- | "Proof" space* enddot { skip_proof lexbuf }
+ | "Proof" space* '.' { skip_proof lexbuf }
| identifier { skip_proof lexbuf } (* to avoid keywords within idents *)
| eof { () }
| _ { skip_proof lexbuf }
and skip_to_dot = parse
- | eof | enddot { if !gallina then gstate := AfterDot }
+ | eof | '.' space { if !gallina then gstate := AfterDot }
+ | ".\n" { if !gallina then gstate := AfterDot; line_break(); }
| "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }