| changeset 70662 | 0f9a4e8ee1ab |
| parent 68880 | 8b98db8fd183 |
| child 73101 | 3d5d949cd865 |
--- a/src/Pure/PIDE/execution.ML Fri Sep 06 16:11:19 2019 +0200 +++ b/src/Pure/PIDE/execution.ML Fri Sep 06 16:48:28 2019 +0200 @@ -141,7 +141,7 @@ val props = if ! Multithreading.trace >= 2 then [(Markup.taskN, Task_Queue.str_of_task task)] else []; - in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end; + in Output.status (map (Markup.markup_only o Markup.properties props) markups) end; type params = {name: string, pos: Position.T, pri: int};