proper nesting of adjacent lists;
authorwenzelm
Thu, 15 Oct 2015 13:28:36 +0200
changeset 61446 9b09acfb7e06
parent 61445 31aadb15eda5
child 61447 7cf8b604280f
proper nesting of adjacent lists;
src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 12:43:02 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 13:28:36 2015 +0200
@@ -85,9 +85,13 @@
 
 fun add_span (opt_marker, body) document =
   (case (opt_marker, document) of
-    (SOME marker, List (list_marker, list_body) :: rest) =>
-      if marker = list_marker then List (list_marker, body @ list_body) :: rest
-      else List (marker, body) :: document
+    (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
+      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
+      else
+        List (marker, body) :: document
   | (SOME marker, _) => List (marker, body) :: document
   | (NONE, _) => body @ document);