# HG changeset patch
# User wenzelm
# Date 1610114631 -3600
# Node ID 693a39f2cddc7f5e7abc3aa03a322bb63dad53f4
# Parent  ccbefeb3a50d27c60868611b2ec794e3f83c89d7
recovered body_range from eca176f773e0 --- its Command.core_range is in conflict with batch-build markup;

diff -r ccbefeb3a50d -r 693a39f2cddc src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 08 14:42:18 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 15:03:51 2021 +0100
@@ -244,8 +244,9 @@
           | SOME 0 => ()
           | SOME n =>
               let
+                val pos = #1 (Toplevel.body_range_of tr);
                 val m = Markup.command_indent (n - 1);
-              in Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) () end)
+              in Toplevel.setmp_thread_position tr (fn () => Position.report pos m) () end)
         else ()
       end
   | NONE => ());