aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/pretty.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/pretty.mll')
-rw-r--r--tools/coqdoc/pretty.mll21
1 files changed, 13 insertions, 8 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 096e64a81..e9fd9c65e 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -325,17 +325,22 @@ rule coq_bol = parse
skip_to_dot lexbuf;
coq_bol lexbuf
end else begin
- indentation (count_spaces s);
- ident s (lexeme_start lexbuf);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
+ 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 }
| space* gallina_kw
{ let s = lexeme lexbuf in
- indentation (count_spaces s);
- ident s (lexeme_start lexbuf);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
+ 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 }
| space* "(**" space+ "printing" space+ (identifier | token) space+
{ let tok = lexeme lexbuf in
let s = printing_token lexbuf in