From 6c65822cd241ea2f5c552f8b685490aed86eecb1 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 16 Aug 2016 17:25:43 +0200
Subject: 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.
---
 tools/coqdoc/cpretty.mll | 30 +++++++-----------------------
 1 file changed, 7 insertions(+), 23 deletions(-)

(limited to 'tools/coqdoc/cpretty.mll')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 9191b2aca..6cf1eaae1 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,_) ->
-- 
cgit v1.2.3