changeset 72704 | e700e830562e |
parent 72703 | eca176f773e0 |
child 72708 | 0cc96d337e8f |
--- a/src/Pure/PIDE/command.scala Wed Nov 25 13:12:31 2020 +0100 +++ b/src/Pure/PIDE/command.scala Wed Nov 25 13:22:34 2020 +0100 @@ -142,7 +142,7 @@ Markup_Index(status, chunk_name) } - (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) + (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML))(body))(_ + _) } }