diff options
Diffstat (limited to 'tools/coqdoc/pretty.mll')
| -rw-r--r-- | tools/coqdoc/pretty.mll | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 2763cb181..6d088a70a 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -229,7 +229,7 @@ let decl_token = let gallina_ext = "Module" - | "Declare" + | "Declare" space+ "Module" | "Transparent" | "Opaque" | "Canonical" @@ -338,26 +338,28 @@ rule coq_bol = parse { end_show (); coq_bol lexbuf } | space* gallina_kw_to_hide { let s = lexeme lexbuf in - if !light && section_or_end s then begin - skip_to_dot lexbuf; - coq_bol lexbuf - end else begin - let s = lexeme lexbuf in - let nbsp = count_spaces s in - indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + if !light && section_or_end s then + begin + skip_to_dot lexbuf; + coq_bol lexbuf + end + else + begin + let nbsp = count_spaces s in + indentation nbsp; + let s = String.sub s nbsp (String.length s - nbsp) in + ident s (lexeme_start lexbuf + nbsp); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | space* gallina_kw { let s = lexeme lexbuf in let nbsp = count_spaces s in + let s = String.sub s nbsp (String.length s - nbsp) in indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + ident s (lexeme_start lexbuf + nbsp); + let eol= body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space* prog_kw { let s = lexeme lexbuf in let nbsp = count_spaces s in |