proper recursive nesting of adjacent lists;
authorwenzelm
Thu Oct 15 16:44:25 2015 +0200 (2015-10-15)
changeset 614533a3e3527445e
parent 61452 fa665e3df0ca
child 61454 c86286ae9fe5
proper recursive nesting of adjacent lists;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:37:14 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:44:25 2015 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4        if marker = list_marker then
     1.5          List (list_marker, body @ list_body) :: rest
     1.6        else if #indent marker < #indent list_marker then
     1.7 -        List (marker, body @ [list]) :: rest
     1.8 +        add_span (opt_marker, body @ [list]) rest
     1.9        else
    1.10          List (marker, body) :: document
    1.11    | (SOME marker, _) => List (marker, body) :: document