diff options
Diffstat (limited to 'tools/coqdoc/pretty.mll')
-rw-r--r-- | tools/coqdoc/pretty.mll | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index e0d2a3c99..9a6bcd568 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -22,12 +22,12 @@ let count_spaces s = let n = String.length s in let rec count c i = - if i == n then c else match s.[i] with + if i == n then c,i else match s.[i] with | '\t' -> count (c + (8 - (c mod 8))) (i + 1) | ' ' -> count (c + 1) (i + 1) - | _ -> c + | _ -> c,i in - count 0 0 + count 0 0 let count_dashes s = let c = ref 0 in @@ -350,27 +350,27 @@ rule coq_bol = parse if eol then (line_break (); coq_bol lexbuf) else coq lexbuf else begin - let nbsp = count_spaces s in + let nbsp,isp = count_spaces s in indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); + let s = String.sub s isp (String.length s - isp) in + ident s (lexeme_start lexbuf + isp); 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 + let nbsp,isp = count_spaces s in + let s = String.sub s isp (String.length s - isp) in indentation nbsp; - ident s (lexeme_start lexbuf + nbsp); + ident s (lexeme_start lexbuf + isp); 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 + let nbsp,isp = count_spaces s in indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); + let s = String.sub s isp (String.length s - isp) in + ident s (lexeme_start lexbuf + isp); let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } @@ -495,7 +495,7 @@ and doc = parse doc lexbuf } | "[[" nl space* { formatted := true; line_break (); start_inline_coq (); - indentation (count_spaces (lexeme lexbuf)); + indentation (fst (count_spaces (lexeme lexbuf))); let eol = body_bol lexbuf in end_inline_coq (); formatted := false; if eol then doc_bol lexbuf else doc lexbuf} @@ -604,7 +604,7 @@ and skip_to_dot = parse and body_bol = parse | space+ - { indentation (count_spaces (lexeme lexbuf)); body lexbuf } + { indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } | _ { backtrack lexbuf; body lexbuf } and body = parse @@ -632,7 +632,7 @@ and body = parse and notation_bol = parse | space+ - { indentation (count_spaces (lexeme lexbuf)); notation lexbuf } + { indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf } | _ { backtrack lexbuf; notation lexbuf } and notation = parse |