changeset 75659 | 9bd92ac9328f |
parent 75393 | 87ebf5a50283 |
child 76975 | 5ba8cb258e75 |
--- a/src/Pure/PIDE/markup_tree.scala Fri Jul 08 20:06:53 2022 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Fri Jul 08 20:24:05 2022 +0200 @@ -258,7 +258,7 @@ body ++= make_text(last, elem_range.stop) make_elems(elem_markup, body.toList) } - make_body(root_range, Nil, overlapping(root_range)) + make_body(root_range, Nil, overlapping(root_range)) } override def toString: String =