proper recursive nesting of adjacent lists;
authorwenzelm
Thu, 15 Oct 2015 16:44:25 +0200
changeset 61453 3a3e3527445e
parent 61452 fa665e3df0ca
child 61454 c86286ae9fe5
proper recursive nesting of adjacent lists;
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