# HG changeset patch
# User wenzelm
# Date 1444920265 -7200
# Node ID 3a3e3527445eb6d7648db6f237bd4d1546d18e70
# Parent  fa665e3df0ca119836ed2779417a3fb4543838fc
proper recursive nesting of adjacent lists;

diff -r fa665e3df0ca -r 3a3e3527445e src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:37:14 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:44:25 2015 +0200
@@ -126,7 +126,7 @@
       if marker = list_marker then
         List (list_marker, body @ list_body) :: rest
       else if #indent marker < #indent list_marker then
-        List (marker, body @ [list]) :: rest
+        add_span (opt_marker, body @ [list]) rest
       else
         List (marker, body) :: document
   | (SOME marker, _) => List (marker, body) :: document