author | wenzelm |
Thu, 15 Oct 2015 16:44:25 +0200 | |
changeset 61453 | 3a3e3527445e |
parent 61452 | fa665e3df0ca |
child 61454 | c86286ae9fe5 |
--- 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