# HG changeset patch
# User wenzelm
# Date 1606306954 -3600
# Node ID e700e830562e65a691a33bfad0e18653831d73f8
# Parent  eca176f773e021db0a62b5df809fb4244fc6a8b9
tuned;

diff -r eca176f773e0 -r e700e830562e src/Pure/PIDE/command.scala
--- 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))(_ + _)
     }
   }