proper nesting of adjacent lists;
authorwenzelm
Thu Oct 15 13:28:36 2015 +0200 (2015-10-15)
changeset 614469b09acfb7e06
parent 61445 31aadb15eda5
child 61447 7cf8b604280f
proper nesting of adjacent lists;
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 12:43:02 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 13:28:36 2015 +0200
     1.3 @@ -85,9 +85,13 @@
     1.4  
     1.5  fun add_span (opt_marker, body) document =
     1.6    (case (opt_marker, document) of
     1.7 -    (SOME marker, List (list_marker, list_body) :: rest) =>
     1.8 -      if marker = list_marker then List (list_marker, body @ list_body) :: rest
     1.9 -      else List (marker, body) :: document
    1.10 +    (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
    1.11 +      if marker = list_marker then
    1.12 +        List (list_marker, body @ list_body) :: rest
    1.13 +      else if #indent marker < #indent list_marker then
    1.14 +        List (marker, body @ [list]) :: rest
    1.15 +      else
    1.16 +        List (marker, body) :: document
    1.17    | (SOME marker, _) => List (marker, body) :: document
    1.18    | (NONE, _) => body @ document);
    1.19