tuned;
authorwenzelm
Wed, 25 Nov 2020 13:22:34 +0100
changeset 72940 e700e830562e
parent 72939 eca176f773e0
child 72941 0471eb6a4b99
tuned;
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))(_ + _)
     }
   }