recovered body_range from eca176f773e0 --- its Command.core_range is in conflict with batch-build markup;
authorwenzelm
Fri, 08 Jan 2021 15:03:51 +0100
changeset 73100 693a39f2cddc
parent 73099 ccbefeb3a50d
child 73101 3d5d949cd865
recovered body_range from eca176f773e0 --- its Command.core_range is in conflict with batch-build markup;
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 => ());