author | wenzelm |
Wed, 25 Nov 2020 13:22:34 +0100 | |
changeset 72704 | e700e830562e |
parent 72703 | eca176f773e0 |
child 72705 | 0471eb6a4b99 |
--- 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))(_ + _) } }