diff options
| author | Guillaume Melquiond | 2016-08-16 17:25:43 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-08-16 17:25:43 +0200 |
| commit | 6c65822cd241ea2f5c552f8b685490aed86eecb1 (patch) | |
| tree | bb99ad7e8a2b7752f35df590e287eb29ba408219 | |
| parent | 3941c270d79c3e3a4be12ba260a2694e523e4229 (diff) | |
Output a break before a list only if there was an empty line (bug #4606).
Moreover, this commit makes sure that an empty line after a list is always
translated into a break. ("StartLevel 1" was excluded, for some reason.)
It also avoids some code duplication. In particular, "stop_item ()" is
defined as "reach_item_level 0", so there is no reason to handle
"StartLevel 1" specially.
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 30 |
1 files changed, 7 insertions, 23 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 9191b2acac..6cf1eaae17 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -681,7 +681,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -742,24 +742,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -769,6 +752,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -777,10 +764,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> |