# HG changeset patch
# User wenzelm
# Date 1610120180 -3600
# Node ID 578a33042aa6c6a6e7b300f3fe62f53d0cb06e1a
# Parent  87067698ae53d5e97f95ffbd370d3408a9ccd964
clarified: command keyword position is sufficient (amending 693a39f2cddc);

diff -r 87067698ae53 -r 578a33042aa6 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 08 15:13:23 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 16:36:20 2021 +0100
@@ -243,10 +243,8 @@
             NONE => ()
           | 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 () => Position.report pos m) () end)
+              let val report = Markup.markup_only (Markup.command_indent (n - 1));
+              in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end)
         else ()
       end
   | NONE => ());
diff -r 87067698ae53 -r 578a33042aa6 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Fri Jan 08 15:13:23 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jan 08 16:36:20 2021 +0100
@@ -146,7 +146,8 @@
             else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
             else {
               line_head(current_line) match {
-                case Some(info @ Text.Info(range, tok)) =>
+                case Some(info) =>
+                  val tok = info.info
                   if (tok.is_begin ||
                       keywords.is_before_command(tok) ||
                       keywords.is_command(tok, Keyword.theory)) 0